Changes between Version 6 and Version 7 of AST

Timestamp:

04/18/11 17:16:34 (15 years ago)

Author:

Stephen Siegel

Comment:

--

AST

@@ -54 +54 @@
        * sequence of elements
  * variable definition
-    * scope
+    * scope (global, input/output, ...)
     * name (together with scope, this uniquely identifies the variable)
     * type
@@ -72 +72 @@
  * statements
    * labels: set of labels associated to this statement.   The labels all correspond to the point of control just before the statement.
-   * assign: lhs:=rhs;  Note statements like x+=a, x*=a will be immediately translated to x:=x+1, x:=x*a, etc.
-      * lhs: LeftHandSideExpression
-      * rhs: expression
-   * assert
+   * assert: this could come from a program language assert or a TASS pragma
       * expr: Expression
-   * assume
+   * assume: these come from TASS pragmas
       * expr: Expression
    * pragma (any kind of pragma, represented as just a string)
       * string: this is an initial form, where the text of the pragma is uninterpreted.   After a certain processing stage, TASS pragmas will be parsed and replaced with more specific nodes.  Non-tass pragmas will just remain as strings and will be ignored by TASS.
-      * assert, assume, invariant, input, output, ...
    * switch statement: this can be used to model C's switch
       * expression: expression that is evaluated
@@ -88 +84 @@
          * statement (or something like that)
    * if-then, if-then-else
-   * while
+   * while: loop.   associated invariant (derived from TASS invariant pragma)
    * for
-   * until
+   * do...until
    * break
    * continue