Changes between Version 19 and Version 20 of C Interface

Timestamp:

09/15/10 10:47:11 (16 years ago)

Author:

Stephen Siegel

Comment:

--

C Interface

@@ -21 +21 @@
 
 {{{
-#pragma TASS assume N>0
+#pragma TASS input {N>0} int
+#define N 25
 }}}
+
+(Note: the "25" will be ignored by TASS.)
 
 == Non-deterministic select statement ==
@@ -35 +38 @@
 
 {{{
-#pragma TASS assert forall {int i | i>=0 && i<N} a[i]>=0
+#pragma TASS assert NAME forall {int i | i>=0 && i<N} a[i]>=0;
 }}}
-
-
-== Loop (joint) invariants ==
-
-Question: how are these expressed in the source code?
-
-Answer:  These are also expressed as pragmas:
-{{{
-#pragma TASS jointinvariant skew(2:1) i == spec.j && k == spec.s + 1
-}}}
-or something like that.
 
 == Library calls ==
@@ -104 +96 @@
     int more = fscanf(fp, "%lf", &tmp);
 
-    #pragma TASS assume tmp>=0.0
+    #pragma TASS assume tmp>=0.0;
     if (more == EOF) break;
     i++;
@@ -127 +119 @@
 Question: what are all the pragmas we will need, and what will be there exact syntax and semantics:
 
-Answer: Here is a proposed list:
+Here is the general pragma grammar for assertion/invariants:
 
- * `#pragma TASS assert <TASS expression>`
-   * verify that the expression is true; report an error if it is not
- * {{{#pragma TASS assume <TASS expression>}}}
+{{{ 
+#pragma TASS [collective|joint]? [assert|invariant] IDENT <expression> [skew <expression>]? ;
+}}}
+
+ 
+Other pragmas:
+ * `#pragma TASS assume <TASS expression>`
    * assume the expression is true, i.e., add the value of this expression to the current path condition
- * {{{#pragma TASS invariant <TASS expression>}}}
-   * this is an (ordinary) loop invariant.   Check that it really is an invariant, and use that fact to compute the state after the loop exit
- * {{{#pragma TASS jointinvariant <TASS expression>}}}
-   * this is a joint loop invariant relating this loop to a loop in the specification program.   Use to check functional equivalence.
- * {{{#pragma TASS ignore}}}
+ * `#pragma TASS ignore`
    * ignore the next statement (typically used for I/O statements that are not relevant)
- * {{{#pragma TASS input <type> <variable>}}}
-   * treat the next element as an input variable.   Could be a preprocessor directory defining an object-type macro.
+ * `#pragma TASS input ['{' assumption-expression '}']? <type> <variable>?`
+   * treat the next element as an input variable.   Could be a preprocessor directory defining an object-type macro.  If preceding a preprocessor object macro, leave out the variable.  The assumption expression is optional and can be used to add an assumption to the initial state.
  * `#pragma TASS system`
    * declares the following function to be "system-level"
  * `#pragma TASS abstract`
    * declares the following function to be abstract (a pure mathematical side-effect free function, like sin(x))
-
-To combine an input with assumption:
-{{{
-#pragma TASS input { N>0 && N*N<M }
-int N;
-}}}
 
 Grammar of TASS expressions:
@@ -158 +144 @@
  * {{{forall {<type> <ident> | expr} expr}}}
  * ditto with {{{exists}}} in place of {{{forall}}}
+ * `PROC[expr].IDENT`
+    * reference to a process-global variable in another process (with pid obtained by evaluating expr)
+ * `PROC[expr]@f.IDENT`
+    * like above, but referring to a local variable in function f in the other process