]> TxlProp – Appendix B: Splits

TxlProp – Appendix B: Splits

This document uses a mixture of HTML and XML, which does not display correctly (as of Fall 2005) using Internet Explorer or Safari. Please use Netscape, Mozilla, Firefox, or possibly Opera.

There are currently three basic kinds of splits in TxlProp:

Simple disjunctions
Primitives with special properties
Loops

Simple disjunctions:

Example: T1 = id, id2 T1 {disjunction} ~= id, id ~= id2, id ~= id3, id T1_o1, T1_o2 T1_o1 T1_o1 ~= Xid2, Xid T1_o2 ~= Xid3, Xid TXL source: define q [id] [id] [id] end define ... deconstruct X J [id] J K [id] deconstruct not X J J J

An orB is true if any of its clauses is true, false if all are false. Each clause is split off into a separate timeline for individual analysis, except clauses already determined false are skipped. A split TID must be consistent with all the assertions of its parent TID, but not vice versa. In other words, anything that will be true at the moment of crisis must not have been false at the previous moment represented by a split TID. In the example above, T1_o1 fails because it is inconsistent with the equality-assertion already made about T1. It cannot be the case that the first two fields in X's value are the same at the crisis point but different earlier. So our hypothesis that the deconstruct not succeeds (which presumably we need in order to get to a crisis point later in the rule) reduces to an assertion that the first and third fields in X are not the same. Hopefully this matches our programmer intuition!

Primitives with special properties

TxlProp contains some reduction rules for built-in primitives that make use of the known properties of each one. Some of these reductions involve creating splits. When a primitive-call with special properties is detected, a split is created and all assertions that refer to that primitive-call are moved into the split, with an appropriate substitution in each case. Here are the primitive-property splits implemented so far:

Index in a zero-length string

The value of [index X ""] is 1 for any X. The value of [index "" Y] is 0 for any Y, except that [index "" ""] is still 1. Situations like [index "" Y] can be split into two cases: Y is an empty string or Y is a nonempty string.

Example: T1 {index-in-a-zerolength-string} index , ""stringlit, TargetT1_iz1,T1_iz2 T1_iz1 = # , Target, 0number T1_iz1 < Old, 1number T1_iz2 < 0number, # , Target T1_iz2 < Old, 0number TXL source: construct N [number] _ [index "" Target] where Old [< N]

Each split contains a defining assertion (“Target is empty” or “Target is nonempty”) as well as an altered version of the original assertion that was split—which for this example was <Old, index , ""stringlit, Target.

Index of a Concat

When [index] is applied to a string-concatenation, either the target string is found within one of the items of the concatenation or the target string is not found anywhere. If found, the result is the position of the target within the chosen item plus the length of all preceding items. If not found, the result is 0.

Example: T1 {index-of-a-concat} index , +concat A, B, C, TargetT1_ic1,T1_ic2,T1_ic3,T1_ic4 T1_ic1 < 0number, index , A, Target T1_ic1 < Old, index , A, Target T1_ic2 < 0number, index , B, Target T1_ic2 = 0number, index , A, Target T1_ic2 < Old, +sum index , B, Target, # , A T1_ic3 < 0number, index , C, Target T1_ic3 = 0number, index , B, Target T1_ic3 = 0number, index , A, Target T1_ic3 < Old, +sum index , C, Target, # , B, # , A T1_ic4 = 0number, index , C, Target T1_ic4 = 0number, index , B, Target T1_ic4 = 0number, index , A, Target T1_ic4 < Old, 0number TXL source: construct X [stringlit] A [+ B] [+ C] construct N [number] _ [index X Target] where Old [< N]

In the example above, there are three items in the concatenation, so there are four splits (found in A; found in B; found in C; not found anywhere). Each split except the last contains assertions that the target string was found within the chosen item and not found within preceding items; the last split asserts that the target was not found within any item. The last assertion of each split is an altered version of the original assertion: <Old, index , +concat A, B, C, Target. In the first case the target is found in A, so we can just get rid of the +concat and the B,C. In the second case it's found in B, so we add the length of A to the result. In the third case it's found in C, so we add the lengths of both A and B. In the final case it's not found anywhere so the result is zero.

Nth of a constructor

For expressions like X, Y where the length of Y is known, we can make a split where each case represents the choice of one element of Y as the value for the nthA. In particular, for situations like X, ... ... where the second parameter of nthA is a literal constructor for a repeat or list, we can have a split where one value from the constructor is substituted in each case.

Example: T1 {nth-of-a-repeat/list} e1, number 1number, 3number, 5number MoreNumsT1_nth1,T1_nth2,T1_nth3,T1_nth4 T1_nth1 = N, 1number T1_nth2 = N, 3number T1_nth3 = N, 5number T1_nth4 = N, +sum e1, -3number, MoreNums TXL source: construct Y [list number+] 1, 3, 5, MoreNums where N [= each Y]

In this example, the selector is an indexvarA, which is eventually bound to all possible values, so there is no point in adding an assert for it to each case. In the “tail” case the nthA must remain, since we don't know anything about MoreNums. Note in the tail case that e1 has become separated from the list it originally referred to, which might make it difficult to determine what its maximum value should be; this area needs further research.

Loop splits

When TxlProp can determine that at least one of the control-variables for a loop is part of a recognizable safe-looping paradigm (see Appendix C), the loop is converted to a split for further analysis. In a loop split, the first case describes the situation where the loop fails to stop iterating after arriving in its terminal state. The other cases (if any) describe situations in which a loop-variable fails to make progress towards its terminal-state value.

Example: T1 <= 1number, length , T1 tail , 2number, next : Param, 1number, , 100number, Paramnext = crisis, number = Paramcrisis, ""stringlit < 2number, 2number <= 1number, , 1number <= # , Param, 100numberT1_loop1,T1_loop2,T1_loop3 T1_loop1 <= 1number, length , number T1_loop2 < 2number, 2number T1_loop3 <= 1number, , 1number <= # , Param, 100number TXL source: function dual Param [stringlit] replace [repeat number] First [number] Rest [repeat number] construct NextParam [stringlit] Param [: First 100] by Rest [dual NextParam] end function

In this example, is a repeat that is shortened by each loop iteration, while Param is a stringlit that is shortened by each(?) iteration. Besides the loop, the only other thing we know is that the scope must be a nonempty repeat (otherwise the replace won't match). The first case describes the terminal state (scope = empty list, param = empty string). The second has the scope not making any progress (the new scope is [tail X] so X must be at least 2 to ensure progress towards empty). The third has Param not making progress (it's [: X Y], so if X = 1 and Y = length of string then there's no progress). loop1 Although the first case is displayed as a conjunction of equalities, it's actually implemented as a set of substitutions which are applied to all assertions with the same TID as the loop. If an assertion is changed by any of the substitutions, the result is added to the loop1 timeline. This produces a set of assertions about what will happen in the terminal state. In this case, substituting an empty string for Param has no effect, but substituting an empty list for leads to a contradiction—so we know that the loop *cannot* continue iterating after the scope becomes empty. Whew! loop2 is obviously false, because [tail 2] cannot fail to make the repeat shorter on every iteration. loop3 is an open issue. If the currently-First element of the repeat happens to be 1 and the length of Param is less than 100, the [:] substring operator won't make the string any shorter, so TxlProp refuses to bless this loop as definitely safe. TxlProp is wrong; this loop is definitely safe because always gets shorter and the loop will end when it becomes empty, no matter what happens to Param. Further refinement is needed.