]> TxlProp – Appendix A: The notation for assertions

TxlProp – Appendix A: The notation for assertions

Get Firefox!
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.

Each crisis point is labelled with a TID, such as T1.  Assertions labelled with the same TID must all be true in order for unsafe behaviour to occur at the crisis point.  The TID can be thought of as identifying a moment in time when the crisis happens. A disjunction is represented as a set of “split TID's”, with derived names such as T1_loop1, T1_loop2, etc..  At least one split TID must have all-true assertions in order for the crisis point to be unsafe.  Splits can be thought of as referring to an earlier point in time, a point when a decision was made as to which branch of a disjunction would be executed.  Splits can have subsplits: T1_loop1_ic1. The timeline T1 → T1_loop1 → T1_loop1_ic1 represents a path leading back from the putative moment of failure toward the start of the program.  In order for a crisis point to be safe, each of its timelines must fail due to a logical contradiction. All assertion clauses appear inside assertions tags.  Assertion clauses contain Boolean expressions, which contain arithmetic expressions.  There are some additional “bits and pieces” tags.  A few tags are for internal use and shouldn't appear in output files.

Assertion clauses:

assertB, assert_failedB, assert_provenB

Boolean expressions:

Basic: B, loopB, matchB, splitB, structureB
Composed: andB, notB, orB
Decided: falseB, trueB

Arithmetic expressions:

Basic: A, constructA, deconstructA, nthA
Data: empty/, literal, varT, zero/
Linkage: rulescopeA, ruleargA

Bits and pieces:

Timelines: prevtids, tid
Identifiers: classT, prim, ruleT
Variables: indexvarA, scope/, varA
Types: class, type
Type bits: attr/, list/, not/, opt/, plus/, repeat/, see/
Pattern bits: construct_tail/, skippingA
Pattern flags: all/, inside/, neg/, new/, srch/
Disambiguators: alpha/, classnth, defalt, extref, loopref, num/
Separators: deconstruct_mark/, split_mark/, structure_mark/

Internal use:

placeholder/, underscore/, unknown_class/, varclass
Form: A  ruleT-or-prim  scope,  params...  /A
Contains: arithmetic expressions, prim, ruleT Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Template:  
Example: index , X, Y TXL source: construct N [number]
  _ [index X Y]
Example: fumble X TXL source: X [fumble]
An arithmetic subroutine call (or string call or list call or any kind of call *except* a Boolean).  The subroutine ruleT-or-prim is applied to scope and optional params.
Form: all/
Contains: (nothing) Part of: constructA
Template:
Example: tailid, 2number, q next TXL source: rule fun7
  replace [q]
    First [id] Rest [repeat id]
  by
    Rest [fun7]
A unification in which both an “exact” match and an “inside” match can occur.  See also inside/.
Form: alpha/
Contains: (nothing) Part of: prim
Template:
Example: <X, "middle"stringlit TXL source: X [< "middle"]
Specifies that a < or <= primitive is using lexicographic ordering.  This enables some reductions in TxlProp's expression-simplifier.  See also num/.
Form: andB  exprs...  /andB
Contains: Boolean expressions Part of: assertB, Boolean expressions
Template:  
Example: < 0number, index , "filename"stringlit, / ~= "filename"stringlit, "/dev/null"stringlit TXL source: construct _ [stringlit]
  _ [write "filename"]
Example: = id, id2 1 id id TXL source: define program
  [id] [id] | [stringlit]
end define
function main
  match [program]
    J [id] J
end function
Logical conjunction.  This tag is rarely seen in final output because assertions with the same TID are implicitly ANDed, so an assertB containing an andB can be replaced by multiple asserts.  But if the AND is obviously true or false, it will be “quick-frozen” within the trueB or falseB and then you can see it. A conjunction is false if any of its exprs is false.  In the second example above, if the structure expression is false, the equality would be meaningless because the fields it refers to don't exist.  That's okay; just one false expr makes the conjunction false, even if the other clauses are undecidable. An AND with no exprs is true.  This is seen in loops that don't terminate because they fail to contain any statements that check for a terminating condition.
Form: assertB  tid  expr  /assertB
Contains: Boolean expressions, tid Part of: assertions, assert_failedB, assert_provenB, splitB
Template:   
Example: T1~= X, 1number TXL source: assert X [= 1]
Expr must be true at time tid in order for the crisis point to be unsafe. The glyph ⊨ is defined in Unicode as “true, valid, is a tautology, satisfies, results in”.
Form: assert_failedB  tid  asserts  /assert_failedB
Contains: assertB, tid Part of: assertions, splitB
Template:     
Example: T1 T1 < X, 10number TXL source: assert
  X [<= 1] [>= 10]
This timeline has failed because one or more of its assertions has been determined to be false. Only the false asserts are shown; the others are deleted.  The ⊨ and T1 for the nested assertB clauses are suppressed for readability. The glyph ☺ is a “smile of relief”: the hypothesis of unsafe program behaviour has been disproved.
Form: assert_provenB  tid  asserts  /assert_provenB
Contains: assertB, tid Part of: assertions, splitB
Template:     
Example: T1 T1 <1number, X T1 < X, 10number TXL source: assert
  X [<= 1] [>= 10]
This timeline is proven because all of its assertions have been determined to be true. The ⊨ and T1 for the nested assertB clauses are suppressed for readability. The glyph ☢ (“radioactive sign”) suggests that running this program is hazardous because it is unsafe for all inputs.
Form: attr/
Contains: (nothing) Part of: class
Template:
Example: id TXL source: construct _ [attr id]
An optional value that is not included in the target program's output.  See also opt/.
Form: B  ruleT-or-prim  scope,  params...  /B
Contains: arithmetic expressions, prim, ruleT Part of: andB, assertB, falseB, loopB, notB, orB, splitB, trueB
Template:  
Example: = X, 1number TXL source: where X [= 1]
Example: isBetween X, Y, Z TXL source: where X [isBetween Y Z]
A Boolean subroutine call.  The subroutine ruleT-or-prim is applied to scope and optional params; the result is either “match” (true) or “no match” (false). For visual harmony, names of built-in primitives like = are displayed here in the same colour as the brackets, rather than their usual colour.
Forms: class  name  /class
class  modifier  name-or-literal  /class
class  modifier  name-or-literal  plus/  /class
Contains: classT, literal, Type bits Part of: constructA, deconstructA, skippingA, structureB
Template:  
Example: number TXL source: construct X [number]
Example: 2 appleid id TXL source: define q
  [number]
| [not 'apple] [id]
end define
...
match [q]
  'orange
Example: "yes"stringlit TXL source: match [list "yes"+]
  "yes", "yes", "yes"
Example: id TXL source: construct X [repeat id+]
  'a 'b 'c
construct Y [repeat id+]
  X [tail 9]
A descriptor for a type.  (TxlProp treats the words type and class as synonymous.)  The “lookahead” modifiers and appear only within structureB tags. The syntax of TXL makes it seem that plus/ is part of the definition of the type; i.e., that it is impossible for a variable of type [list id+] to contain an empty list.  This is not true.  The plus/ affects only unification.  Other operations (such as [tail]) can yield an empty sequence of a -type.
Form: classnth  number  /classnth
Contains: plain text Part of: deconstructA
Template:  
Example: number2 TXL source: define q
  [number] [id] [number]
end define
...
match [q]
  1 'middle X [number]
Indicates which field in a nonterminal is being accessed, if the nonterminal has several fields of the same type. Number is always at least 2 because classnth is omitted when referring to the first field of a given type.
Form: classT  name  /classT
Contains: plain text Part of: class
Template: red
Example: id TXL source: skipping [id]
An identifier that has been typed as a class-name (= type-name in TXL). See also type, which means the same thing but is used inside literal tokens.
Forms: constructA  type  opt-defalt  fields  /constructA
constructA  type  fields  construct_tail/  tail  /constructA
constructA  opt-skipping  patflags  type  opt-defalt  fields  /constructA
constructA  opt-skipping  patflags  type  fields  construct_tail/  tail  /constructA
Contains: arithmetic expressions, class, construct_tail/, defalt, pattern flags, skippingA, varclass Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Templates:   
   
   
Example: pair2 "x"stringlit, aid TXL source: define pair
  [id] [number]
| [stringlit] [id]
end define
...
construct P [pair]
  "x" 'a
Example: number TXL source: match [repeat number]
  %Empty
Example: q "x"stringlit, aid, 27number
q id , "x"stringlit, id aid, 27number 		TXL source: define q
  [opt id] "x" [opt id] [number]
end define
...
match * [q]
  "x" 'a 27
Example: , xx A, B C TXL source: skipping [x]
match [list x]
  A [x], B [x], C [list x]
A literal value of a complex type, composed from fields.  The constructA tag has ended up being a general workhorse in TxlProp, performing a variety of related functions; perhaps it should be split into several tags for the furtherance of clarity.  Basic functions performed:
  • Literals for nonterminal types defined in the grammar.
  • Literals for sequence types.
  • Literals for optional/attribute types.
  • Casts.
  • Patterns.
Early parsing of complex literals produces constructA tags that have the flag.  These contain fields that match the TXL source.  Later these are elaborated with empty constructors and casts, so for every field in the nonterminal there is a matching field in the constructA. For nonterminals that have multiple productions, the defalt specifies which one this constructor produces. For sequences there are two special cases: a tail can be specified or the sequence can be empty.  For empty constructors an empty/ tag is inserted as a visual comment. An optional/attribute item is either empty or present.  If present, the constructor is effectively a cast that changes the type of the item from x to x or x.  Also cast-like is the use of a constructor for a nonterminal that contains only one field. The skipping and patflags (except for new/) really have nothing to do with construction of literals.  They specify how to use this literal as a match-pattern and thus make sense only when the constructA is the second parameter to an enclosing matchB. The glyphs ⌠ ⌡ are supposed to look like oddly-shaped brackets.  Also the glyphs ⌠ ∫ ⌡ should form a visually-related set.
Form: construct_tail/
Contains: (nothing) Part of: constructA
Template:
Example: xA, B C TXL source: replace [list x]
  A [x], B [x], C [list x]
A sequence-constructor consisting of one or more “head” items of the base type, followed by a pre-formed “tail” of the sequence type.
Forms: deconstructA  value  deconstruct_mark/  field  /deconstructA
deconstructA  value  deconstruct_mark/  field  classnth  /deconstructA
Contains: arithmetic expressions, class, classnth, deconstruct_mark/, varclass Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Templates:  
  
Example: id
id2 		TXL source: define Q
  [id] "x" [id]
end define
...
match [Q]
  Left [id] "x" Right [id]
Accessor for a field within a value (whose type is a nonterminal defined in the grammar).  The field is named by its type.  If the nonterminal defines several fields of the same type, the optional classnth parameter will indicate which one is intended (default is leftmost one). If value's type has multiple productions, a separate structureB assertion will be emitted to indicate which production the deconstructor refers to.  When the time comes to access the actual field-data, the value will have been reduced to a constructA literal, which will also have a defalt tag to specify which production is intended. The glyph ↯ is supposed to be suggestive of tree-traversal.
Form: deconstruct_mark/
Contains: (nothing) Part of: deconstructA
Template:
Example: id TXL source: define pair
  [number] [id]
...
match [pair]
  2 Name [id]
Separates the value being deconstructed from the type of the field being accessed.
Form: defalt  num  /defalt
Contains: plain text Part of: constructA, structureB
Template:  
Example: 2 number
q3 doneid 		TXL source: define q
  [charlit] | [number] | [id]
end define
...
replace [q]
  _ [number]
by
  done
Specifies which alternative production is intended, when referring to nonterminals that have several productions.
Form: empty/
Contains: (nothing) Part of: B, constructA
Template:
Example: id TXL source: match [repeat id]
  %Empty
Example: = stringlit, TXL source: define program
  [opt stringlit] [id]
end define
...
match [program]
  X [id]
Representation for empty sequences and for optional elements that are not present. The use of for empty sequences is just a visual comment.  The constructor behaves as if it contained zero expressions.
Form: extref  eid  /extref
Contains: plain text Part of: varT
Template:  
Example: id 1number, Globali1, 1number, Globali2 TXL source: import Global [repeat id]
  G1 [id] _ [repeat id]
...
import Global
  G2 [id] _ [repeat id]
export Global
  G1 G2
Disambiguates the bindings for a variable that come from different import statements.  This prevents distinct imported values from comparing as “equal” because they have the same name. Currently, TxlProp does not track export bindings and match them with imports, so crisis points whose safety depends on imported values are not decidable as true or false.
Form: falseB  expr  /falseB
Contains: Boolean expressions Part of: assertB, Boolean expressions
Template:  
Example: ~= 4number, 4number TXL source: construct N [number]
  4
where
  N [~= 4]
The expr has been determined to be false. TxlProp's expression simplifier tries to be cute: when it determines that an expression is false, it puts a   wrapper around the original expression, as of the start of the simplification pass that led to the “false” determination.  Sometimes this goes too far, presenting a gigantic expression marked with falseB without showing any of the proof-steps that led to that conclusion.  Sometimes it doesn't go far enough, leaving trivial stuff like singleton +sum X that would make more sense if simplified to X. The content of a falseB tag is “frozen”: future simplification passes will not touch it.
Form: indexvarA  name  /indexvarA
Contains: plain text Part of: varT
Template:  
Example: e1, X TXL source: [funcall each X]
Example: tail , m1, next TXL source: rule test
  replace [repeat id]
    X [repeat id]
  by
    X
end rule
A generated variable which is an index into a sequence.  The variable is an integer with minimum value 1 and maximum value equal to the length of the sequence that it indexes.
Form: inside/
Contains: (nothing) Part of: constructA
Template:
Example: , q next TXL source: rule fun8
  replace $ [repeat q]
    Q [repeat q]
  by
    Q [fun8]
A unification in which the pattern is not permitted to match the entire replacement, but may match some node inside it.
Form: list/
Contains: (nothing) Part of: class
Template:
Example: number TXL source: match [list number]
A comma-separated sequence.
Forms: literal  data  /literal
literal  data  type  /literal
Contains: plain text, type Part of: Basic arithmetic expressions, Basic Boolean expressions, class, varclass
Templates:  
   
Example: * TXL source: '*
Example: 1.2e+17number TXL source: 1.2e+17
Example: I_am_not_a_variableid TXL source: I_am_not_a_variable
Example: 'x'
'y'charlit 		TXL source: define q
  [id] ''x' [charlit]
end define
...
match [q]
  A [id] ''x' ''y'
A literal token.  Most literals have a marking for their type, but punctuation marks and compounds do not (internally TXL types them as *literal).  When a literal in a pattern is matched with a literal in a nonterminal's production, its type is removed to represent the fact that production-literals must match pattern-literals, not variables that happen to be of the same type. Numbers, stringlits, and sometimes identifiers are self-quoting; TxlProp acts as if the apostrophe were always present.  Identifiers are self-quoting in a define and when not (yet) declared as a variable within a rule or function.  Charlits are self-quoting if they don't contain spaces, but TxlProp doesn't handle this and always requires a double-apostrophe for charlits.
Form: loopB  matches...  /loopB
Contains: matchB, orB Part of: assertB, falseB, splitB
Template:  
Example: +sum, 1number, next Label, Labelnext TXL source: rule fun1  Label [stringlit]
  replace [number]
    N
  by
    N [+ 1] [putp Label]
end rule
Example: X, fun2 TXL source: construct _ [id]
  X [fun2] %Fun2 calls me back
Example: Q, next Q2, next TXL source: define Q
    [stringlit]
  | [id] [Q] [Q]
end define
rule fun3
  replace $ [Q]
    Old
  by
    Old [putp "Val: "]
end rule
The matches specify the next-iteration values for the scope and parameters.  Usually the next value is computed from the current value; in some cases the current value is passed along as-is.  If any matchB in the loop is false (no matches possible), the loop is false (no iterations possible). If the loop crosses a rule-boundary, TxlProp currently leaves dangling references to the scope and parameters of the next rule in the loop. For replace $ loops, an orB can arise if there are several spots within the new scope where the next iteration can match. If a safe-looping paradigm is detected, the loop can be converted to a split as the next step in the disproof process.  See Appendix C for a list of the safe-looping paradigms currently recognized.
Form: loopref  subtype  /loopref
Contains: plain text Part of: varT
Template:  
Example: foo , next Param, Paramnext= crisis, L1 = Paramcrisis, Paraminitial TXL source: function try Param [id]
replace [id]
  X [id]
by
  X [foo] [try Param]
end function
Disambiguates the bindings for a variable in different iterations of a loop.  Currently the following contents are defined:
  • (no loopref): The current iteration.
  • next: The next iteration.
  • initial: The first iteration.
  • crisis: The iteration when the loop goes crazy.
  • Ln: Some value that TxlProp cannot compute because it doesn't recognize the looping paradigm.  These are generated identifiers to ensure that multiple incomputable values don't compare “equal”.
Form: matchB  replacement,  pattern  /matchB
Contains: arithmetic expressions Part of: andB, assertB, falseB, loopB, notB, orB
Template:  
Example: X, 1number TXL source: deconstruct X
  1
Example: , id aid, B C TXL source: replace [repeat id]
  'a B [id] C [repeat id]
Example: Xlist, numberX TXL source: deconstruct * [number] Xlist
  X [number]
Unification-match between pattern and replacement.  For syntactic reasons, the match-flags (*, $, ALL) actually appear as part of the pattern, where they are called pattern flags.  If no flags are present, this is an “exact match”. TXL deconstructs the replacement to produce bindings for the variables in pattern, but TxlProp (because it is working backwards from crisis points) substitutes replacement for pattern wherever it appears in other assertions.  If no matches are possible, the matchB assertion is false. If the pattern is a literal or an already-bound variable, substitution cannot be performed.  Instead TxlProp will produce an assertion that the replacement has the required value. If the pattern is a constructA, the substitutions for its fields will involve nthA and/or deconstructA tags applied to the replacement.  If pattern contains defalt, an assertion containing structureB will be generated to represent the requirement that the replacement must match the specified grammar-production. For negated matches —   —  no substitutions occur.  Instead a set of assertions is generated to state that some replacement-part fails to have the required value.
Form: neg/
Contains: (nothing) Part of: constructA
Template:
Example: X, number 4number
X, 4number 		TXL source: deconstruct not X
  4
A negated pattern.  Not seen in output because it is always replaced by a negated match. Note that neg/ (the pattern flag) and notB (the Boolean operator) both display as "not", but with different coloured backgrounds.  The tag not/ is a class-modifier and is unrelated.
Form: new/
Contains: (nothing) Part of: constructA
Template:
Example: q "marker"stringlit
q id, "marker"stringlit 		TXL source: define q
  [opt id] [stringlit]
end define
...
match [q]
  "marker"
A newly-constructed literal whose contents matches the TXL source rather than the nonterminal's definition in the grammar.  These new constructors are then replaced by elaborated constructors that contain the omitted fields, casts, etc. The flag appears in final output in cases where the elaborator was unable to understand the nonterminal's productions.  This can happen because the elaborator currently does not offer backtracking or support for left-recursion.  Some constructors in file "AVL.module" have this problem.
Form: not/
Contains: (nothing) Part of: class
Template:
Example: 1 beginid id TXL source: define q
  [not 'begin] [id]
| [repeat id]
end define
...
match [q]
  'test
Block the pattern-match if the next item has the given class or literal value.  Since no value is bound to variables, this modifier appears only in structureB tags.
Form: notB  expr  /notB
Contains: Boolean expressions Part of: assertB, Boolean expressions
Template:  
Example: X, 1number TXL source: deconstruct not X
  1
Logical negation.  Rarely seen in final output because most occurrences of notB are eliminated by using DeMorgan's theorem, or changing a primitive from = to ~=, etc.
Form: nthA  nth,  sequence /nthA
Contains: arithmetic expressions Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Template:  , 
Example: T1 <= 1number, length , T1 ...  1number,  ... TXL source: match [repeat id]
  First [id] Rest [repeat id]
Example: e1, stringlit "a"stringlit, "b"stringlit, "c"stringlit
e1, stringlit "one"stringlit, "two"stringlit, "three"stringlit 		TXL source: construct Files [repeat stringlit]
  "a" "b" "c"
construct Labels [list stringlit]
  "one", "two", "three"
construct _ [number]
  _ [fputp each Files Labels]
Accessor for the nth field within sequence (a list or repeat). When TxlProp generates an nthA tag, it also generates an assertion that the sequence is long enough to actually have an nth field.  In the first example above, the nthA is meaningless if the scope is an empty repeat, but in that case the <= will fail and so the value of nthA won't matter. For each arguments, an nthA is produced whose nth is an indexvarA.  No side assertion is generated since the indexvarA will iterate through all valid values.  For each followed by two variables, both nthA tags refer to the same indexvarA to represent the fact that corresponding fields are selected for each iteration.
Form: num/
Contains: (nothing) Part of: prim
Template:
Example: <=X, 47number TXL source: X [<= 47]
Specifiesthat a < or <= primitive is using numeric ordering.  This enables some reductions in TxlProp's expression-simplifier.  See also alpha/.
Form: opt/
Contains: (nothing) Part of: class
Template:
Example: number TXL source: replace [opt number]
An optional value that *is* included in the target program's output (unlike attr/ which is not included but otherwise the same).
Form: orB  exprs  /orB
Contains: Boolean expressions Part of: assertB, Boolean expressions
Template:  
Example: 1 id ~= id, aid TXL source: define program
  [id] | [stringlit]
end define
...
match [program]
  X [program]
deconstruct not X
  'a
Logical disjunction.  This tag is rarely seen in final output because an orB is usually converted to splitB so the exprs can then be analyzed separately.  But if the OR is obviously true or false, it will be “quick-frozen” within the trueB or falseB and then you can see it. A disjunction is true if any of its exprs is true.  In the example above, if the structure expression is false, the inequality would be meaningless because the field it refers to doesn't exist.  That's okay; just one true expr makes the disjunction true, even if the other clauses are undecidable.
Form: placeholder/
Contains: (nothing) Part of: arithmetic expressions, Boolean expressions
Template:
A marker that indicates “no expression yet”.  Used internally as part of the construction process for expressions.  Should never appear in output files!
Form: plus/
Contains: (nothing) Part of: class
Template:
Example: id TXL source: match [repeat id+]
Patterns with this modifier will not match an empty sequence.
Form: prevtids  tids...  /prevtids
Contains: tid Part of: splitB
Template:  
Example: T1{index-in-a-zerolength-string} index , ""stringlit, XT1_iz1,T1_iz2 TXL source: _ [index "" X]
Connects a timeline with a set of alternative timelines that preceded it. In this example, if a crisis happens at T1, then before that either T1_iz1 happened (X was bound to an empty string) or T1_iz2 happened (X was bound to a nonempty string).
Form: prim  name  /prim
Contains: alpha/, num/, plain text Part of: A, B
Template: purple
yellow
Example: +sum X, Y TXL source: X [+ Y]
Example: istype X, numberid TXL source: X [istype 'number]
Example: < X, "z"stringlit TXL source: X [< "z"]
A name for a built-in primitive function.  These can be identifiers (index), punctuation marks (~=) or compounds (+concat). To reduce the number of expression-simplification rules, TxlProp converts the greater-than operators to less-than forms: X [> Y] becomes < Y, X, while X [>= Y] becomes <= Y, X. TXL has some pairs of built-in functions that have the same name but different types.  TxlProp disambiguates them: [+] becomes +sum for numbers, +concat for other tokens, while [<] and [<=] become < and <= for numbers, < and <= for other tokens. In some cases, TXL allows built-in primitives to be overridden by source-code rules with the same name, so TxlProp disambiguates a rule-name as ruleT if defined, prim if not defined—it has no explicit list of all known primitives.  TxlProp's expression-simplifier has special reductions for built-in rules such as index; these reductions do not apply to a user-override index. TxlProp introduces some “primitives” which do not correspond to anything in TXL.  These have names beginning with dollar signs: $max.
Form: repeat/
Contains: (nothing) Part of: class
Template:
Example: id TXL source: match [repeat id]
A space-separated sequence.
Form: ruleT  name  /ruleT
Contains: plain text Part of: A, B, ruleargA, rulescopeA
Template: magenta
Example: fun5Val TXL source: construct _ [number]
  Val [fun5]
Example: fun6Val TXL source: where
  Val [fun6]
A name that refers to a rule or function defined in the target program's source code (i.e., not a built-in primitive).
Form: ruleargA  rule,  argnum  /ruleargA
Contains: plain text, ruleT Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Template:  
Example: Left, Y, 1
Right, Y, 2 		TXL source: X [Y Left Right] %Y calls me back
A positional reference to the parameter of another rule.  As the assertion is repeatedly raised from callee-rule to caller-rule, eventually it will arrive at the target rule and then rulearg will be replaced by the rule's parameter numbered argnum. Currently TxlProp does not raise assertions to callers, so rulearg references are never resolved.
Form: rulescopeA  ruleT  /rulescopeA
Contains: ruleT Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Template:  
Example: X, Y TXL source: X [Y] %Y calls me back
A reference to the scope of another rule.  As the assertion is repeatedly raised from callee-rule to caller-rule, eventually it will arrive at the target rule and then rulescope will be replaced by scope/. Currently TxlProp does not raise assertions to callers, so rulescope references are never resolved.
Form: scope/
Contains: (nothing) Part of: varT
Template:
Example: , 2number TXL source: match [number]
  2
A variable that refers to the input matched by the current function.  This usage is slightly different from that of the txldb program, whose ‘scope’ command shows the entire object that the current function may have matched only part of.
Form: see/
Contains: (nothing) Part of: class
Template:
Example: 1 beginid id TXL source: define q
  [see 'begin] [repeat id]
| [id]
end define
...
match [q]
  begin middle end
Block the pattern-match *unless* the next item has the appropriate class or literal value.  Since no value is bound to variables, this modifier appears only in structureB tags.
Form: skippingA  type  /skippingA
Contains: class Part of: constructA
Template:  
Example: X, foobar Y TXL source: skipping [attr foo]
deconstruct * [bar] X
  Y [bar]
The TXL “skipping” statement precedes a replace/match/deconstruct, but in TxlProp it is syntactically part of the pattern.
Forms: splitB  comment  clause  asserts...  prevtids  /splitB
splitB  loopB.../loopB  split_mark/  expr  asserts...  prevtids  /splitB
Contains: arithmetic expressions, assert_failedB, assert_provenB, Boolean expressions, plain text, prevtids Part of: assertB, falseB, trueB
Templates:  
 
Example: {index-of-a-concat} index , +concat X, Y, ZT1_ic1,T1_ic2,T1_ic3 TXL source: construct C [stringlit]
  X [+ Y]
construct N [number]
  _ [index C Z]
Example: +sum, 1number, next Label, Labelnext = crisis, 10000000number
= Labelcrisis, Labelinitial T1_loop1 		TXL source: rule fun1  Label [stringlit]
  replace [number]
    N
  by
    N [+ 1] [putp Label]
end rule
Example: T1 T1 tail , 2number, next = crisis, id < 2number, 2number T1_loop1,T1_loop2 T1_loop1 T1_loop1 <= 1number, length , id T1_loop2 T1_loop2 < 2number, 2number TXL source: function test
  replace [repeat id]
    First [id] Rest [repeat id]
  by
    First Rest [test]
end function
The important part of a split is the prevtids; everything else is commentary.  The prevtids connect this assertion with a set of split TID's.  At least one split TID must be true in order for this assertion to be true. Splits have a variety of uses.  See Appendix B for a list of the kinds of splits currently implemented. If all split TIDs fail, they are moved inside the splitB to help keep the XML organized.  Similarly, if at least one split TID is proven, all the proven ones are moved inside and the others are deleted.
Form: split_mark/
Contains: (nothing) Part of: splitB
Template:
Example: +sum , 1number, next = crisis, 10000000number TXL source: replace [number]
  X [number]
by
  X [+ 1]
For a loop split, separates the description of the loop-variables from the values they must have at the moment when the loop goes crazy.
Form: srch/
Contains: (nothing) Part of: constructA
Template:
Example: q, q next TXL source: function fun9
  replace * [q]
    'foo Q [repeat q]
  by
    Q [fun9]
A unification in which the pattern can either match the entire replacement or something inside it.  If the latter, only the first (via depth-first traversal) inside match will occur.
Form: structureB  value  structure_mark/  defalt  items...  /structureB 
Contains: arithmetic expressions, class, defalt, literal, structure_mark/ Part of: andB, assertB, falseB, notB, orB, trueB
Template:  
Example: 2 id "z"stringlit TXL source: define Q
  [stringlit] | [id] "z"
end define
...
replace [Q]
  X [id] "z"
True if the format of value (whose type is a nonterminal with multiple productions in the grammar) is that of its production numbered defalt.  The items are just a recitation of the contents of the defalt production and are effectively a comment. Structure assertions are generated as side-effects when matchB clauses are processed, if the match-pattern has a defalt.  In the example above, id can be substituted wherever X appears, but only if actually contains an [id]; if it contains a [stringlit] then the rule will not match, the crisis point will not be reached, and therefore no safety violation can occur at the crisis point.
Form: structure_mark/
Contains: (nothing) Part of: structureB
Template:
Example: 2 id id TXL source: define item
  [number] | [id] [id]
...
match [item]
  Name1 [id] Name2 [id]
Separates the value whose nonterminal structure is being asserted from the description of the field structure it must have.
Form: tid  id  /tid
Contains: plain text Part of: assertB, assert_failedB, assert_provenB, prevtids
Template: T 
Example: T1=X, 1number TXL source: assert X [~= 1]
A timeline identifier.
Form: trueB  expr  /trueB
Contains: Boolean expressions Part of: assertB, Boolean expressions
Template:  
Example: = 4number, 4number TXL source: construct N [number]
  4
where
  N [= 4]
The expr has been determined to be true. TxlProp's expression simplifier tries to be cute: when it determines that an expression is true, it puts a   wrapper around the original expression, as of the start of the simplification pass that led to the “true” determination.  Sometimes this goes too far, presenting a gigantic expression marked with trueB without showing any of the proof-steps that led to that conclusion.  Sometimes it doesn't go far enough, leaving trivial stuff like singleton +sum X that would make more sense if simplified to X. The content of a trueB tag is “frozen”: future simplification passes will not touch it.
Form: type  name  /type
Contains: plain text Part of: literal
Template: red
Example: 1number TXL source: 1
The type-identifier for a literal token.  Same meaning as classT but a less-obtrusive appearance.  The type of 1number is number.
Form: underscore/
Contains: (nothing) Part of: constructA
Template:
Example: index number , "haystack"stringlit, 'needle'charlit TXL source: construct N [number]
  _ [index "haystack" ''needle']
A marker that corresponds to TXL's “_” meaning “default value for this type”.  Eliminated by the constructor-elaborator; should never appear within assertions tags in final output files. Many of the tags documented in this appendix are also used as part of the pretty-printing of the TXL source code.  underscore/ properly appears in output files as part of source code.
Form: unknown_class/
Contains: (nothing) Part of: (internal use)
Template:
A placeholder that indicates “type not yet determined”.  Used internally as part of the constructor-elaboration process.  Should never appear in output files!
Form: varA  name  /varA
Contains: plain text Part of: varT
Template: anon
Example: number anon1, 14number TXL source: match [repeat number]
  _ [number] 14
A generated name for an anonymous variable.  This should not be seen in final output, but does appear in cases where TxlProp's elaborator was unable to deal with a constructor (so varA is always seen together with new/).
Forms: varT  name-or-scope  /varT
varT  name-or-scope  loopref  /varT
varT  name  extref  /varT
varT  varA-or-indexvarA  /varT
Contains: extref, indexvarA, loopref, plain text, scope/, varA Part of: Basic arithmetic expressions, Basic Boolean expressions, varclass
Templates: Blue Blue  Blue  Black
Example: *X, 2number TXL source: X [* 2]
Example: =, 2number TXL source: match [number]
  2
Example: Param, Paramnext TXL source: function fun4  Param [number]
replace...
by
  _ [fun4 Param]
Example: =Xi7, 2number TXL source: import X [number]
  2
Example: number anon1, Val TXL source: match [repeat number]
  _ [number] Val
Example: e1, X TXL source: [funcall each X]
An identifier that has been typed as a variable name.  scope/ is basically just a variable with a special name.  loopref disambiguates bindings that the variable has during different loop-iterations.  extref disambiguates bindings that the variable receives from different import statements.  varA and indexvarA are variables with generated names.
Form: varclass  expr  /varclass
Contains: arithmetic expressions Part of: constructA, deconstructA
Template:  
Example: X "test"stringlit TXL source: import X [repeat stringlit]
import X
  "test"
During TxlProp's “migration phase” (a backward scan from crisis points towards the tops of rules), it sometimes needs to refer to the type of an object whose declaration it has not yet seen.  When the declaration is eventually seen, the varclass is replaced with the actual type. The presence of varclass in the grammar of assertion-notation creates problems, because it means that arithmetic expressions can appear wherever a class is expected.  During TxlProp's self-analysis it thinks that expression-recursions can match in more places than they really can because all occurrences of varclass should have been eliminated by the end of the migration phase.  Perhaps this would be a good use for “agile parsing”: define varclass only for the first two phases of stage 3 and abort at that point if not all of them got resolved.  From then on the set of types and the set of arithmetic expressions would be disjoint.
Form: zero/
Contains: (nothing) Part of: A
Template:
Example: index , X, Y TXL source: construct N [number]
  _ [index X Y]
Representation for the scope of certain primitives (index, length, #) which syntactically require a numeric scope but don't care what its value is. The meaning is exactly the same as 0number, but less visually intrusive.



©2005 by Jonathan Yavner.