]> TxlProp – Appendix C: Safe-looping paradigms

TxlProp – Appendix C: Safe-looping paradigms

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.

TxlProp examines the matchB for each variable in a loop, comparing with its known paradigms for safe looping. For each variable it produces a substitution for its terminal-state value, and in some cases it also produces an assertion describing how the variable might fail to arrive at its terminal state. See ‘loop splits’ in Appendix B for more information on how these results are used.

Inscrutable value:

Example:

foo tail , 2number, next

= crisis, L1

TXL source:

function dump replace [repeat number] First [number] Rest [repeat number] by Rest [foo] [dump] end function

When TxlProp cannot match a loop-variable with any known safe-looping paradigm, it generates an Ln symbol to represent the unknown value. In many cases it is still possible to prove a loop safe even if some of its variables have inscrutable values. If all loop-variables are inscrutable, the loopB is not converted to a splitB. (It would be pointless, since nothing new can be proven by substituting unknowns for explicit values!)

Unchanging value:

Example:

Label, Labelnext

= Labelcrisis, Labelinitial

TXL source:

function dump Label [stringlit] replace [repeat number] First [number] Rest [repeat number] by First [putp Label] Rest [dump Label] end function

If the variable's value does not change from one loop iteration to the next, its value at crisis will be the same as its initial value when the loop started. This is displayed as an equality, but actually unchanging values do not get any substitution. In the terminal-state assertions, any references to Label remain as-is. If all loop-variables are unchanging, the loop is of course unsafe:

Example: T1 , next = crisis, initialT1_loop1 T1_loop1 T1_loop1 T1 ~= , ""stringlit TXL source: function scan replace [stringlit] X [stringlit] deconstruct not X "" by X [: 1 32767] [scan] end function

This function seems to contain a typo: the 1 should perhaps be a 2. As written, the scope is unchanging. When TxlProp converts the loopB to a splitB, it can't find anything to put into the T1_loop1 split, because there is no assertion labelled T1 that has a change when the (empty) list of substitutions is applied. The result is a split consisting of an andB containing zero clauses, which is true. We conclude that this loop will never stop once it gets started, but it won't start if the initial scope is an empty string.

Literal:

Example:

"Next: "stringlit, Labelnext

= Labelcrisis, "Next: "stringlit

TXL source:

function scan Label [stringlit] replace [stringlit] X [stringlit] by X [putp Label] [scan "Next: "] end function

Sometimes a variable has the same literal value for every loop-iteration other than the first. At crisis the variable will have the literal value.

Substring:

Example: T1 : , L, R, next L, Lnext R, Rnext = crisis, ''charlit = Lcrisis, Linitial = Rcrisis, Rinitial <= L, 1number <= # , , RT1_loop1,T1_loop2 TXL source: rule dribble L [number] R [number] replace [charlit] X [charlit] by X [: L R] end rule

The next-iteration value is a substring of the current-iteration value. If the loop is unsafe, either it can continue iterating with an empty string or it can fail to make the string shorter (because L is not more than 1 and at the same time R is not less than the length of the string).

Tail:

Example: T1 , next tail Param, , Paramnext = crisis, initial = Paramcrisis, id < , 2numberT1_loop1,T1_loop2 TXL source: function short Param [repeat id] replace [number] X [number] construct NewParam [repeat id] Param [tail X] construct _ [number] X [short NewParam] by 0 end function

The next-iteration value is a tail of the current-iteration value. If the loop is unsafe, either it can continue iterating with an empty sequence or it can fail to make the sequence shorter (because X is less than 2).

Example: T1 T1 tail , 3number, next = crisis, q < 3number, 2numberT1_loop1,T1_loop2 T1_loop1 T1_loop1 <= 2number, length , q T1_loop2 T1_loop2 < 3number, 2number TXL source: function try replace [list id] X [q], Y [q], Rest [list q] by Rest [try] end function

In this example, the call to tail is implied (because Rest matches [tail 3] of scope). Also implied is that the length of scope must be at least 2 (so X and Y will have something to match). This loop is safe because it cannot continue iterating with an empty list and it cannot fail to make the list shorter on every iteration.

Addition:

Example: T1 < 0number, Addend T1 +sum , Addend, next Addend, Addendnext = crisis, 10000000number = Addendcrisis, AddendinitialT1_loop1 TXL source: rule plus Addend [number] where Addend [> 0] replace [number] Old [number] by Old [+ Addend] end rule

The next-iteration value is the current value plus some positive offset. The loop is unsafe if it can continue iterating when the value reaches ten million. This “magic number” arises because of TXL's limited range for integers: once a number reaches 1e7, TXL switches to a floating-point format with a seven-digit mantissa, so further additions of 1 will have no effect (1e7+1 is still 1e7). If the loop can continue past 10,000,000 then it can continue forever. There is no assertion about the loop failing to make progress, because Addend must be clearly positive in order for this paradigm to be recognized. If Addend is known to be at least 10, then the loop can continue up to 100 million without getting stuck (1e7+10=1.000001e7 but 1e8+10 is still 1e8 ). This paradigm could be further refined.

Subtraction:

Example: +sum , -1number, next = crisis, -10000000numberT1_loop1 TXL source: rule minus replace [number] Old [number] by Old [- 1] end rule

The next-iteration value is the current value minus some offset. The loop is unsafe if it can continue iterating when the value reaches negative ten million. Again there is no assertion about failure to progress because the offset must be clearly negative in order to recognize this paradigm.

Constructor:

Example: T1 <= 1number, length , id T1 program +sum number, 1number, foo number2, tail id, 2number, next = crisis, program 10000000number, foo L1number2, id < 2number, 2numberT1_loop1,T1_loop2 T1_loop1 <= 1number, length , program 10000000number, foo L1number2, id id T1_loop2 < 2number, 2number TXL source: define program [number] [number] [repeat id] end define ... rule nonterminal replace [program] N [number] M [number] F [id] R [repeat id] by N [+ 1] M [foo] R end rule

If the next-iteration value is a constructor, TxlProp uses the next-value and current-value for each field, applying all its paradigms recursively. In this example, the constructor is for a nonterminal with two numbers and a repeat. The first number is incremented (so the loop needs to stop at ten million), the second number has something strange done to it, and the repeat is shortened (so the loop needs to stop at empty). It might seem onerous to insist that the new value for a field must be based on the old value for the same field, but in practice most loops that can be recognized at all will meet this requirement.

Sequence constructor with tail:

Example: T1 <= 2number, length , T1 id 1number, tail , 3number, next = crisis, id 1number, L1 < 3number, 3numberT1_loop1,T1_loop2 T1_loop1 <= 2number, length , id 1number, L1 T1_loop2 < 3number, 3number TXL source: function main replace [repeat id] X [id] Y [id] R [repeat id] construct Result [repeat id] X R by Result [main] end function

If the next-iteration value is a constructor for a sequence, it can have a tail. The loop is safe if the tail is shortened by more than the number of other fields in the constructor (so the sequence as a whole will be getting shorter). In this example, at crisis the repeat will contain one item (shown here as an nthA from some inscrutable previous iteration, although actually it's still the first element from the initial iteration). Since the replace requires at least two items for a match, the loop is safe.