Changes between Version 43 and Version 44 of ContractReduction

Timestamp:

12/14/15 10:53:04 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -12 +12 @@
 * `reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause
 * additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope is used
-* wildcard term: `\everything`
+* wildcard term: `...`
 
 {{{
@@ -35 +35 @@
 completeness-clause ::= complete behaviors (id (, id)∗)? ;
                       | disjoint behaviors (id (, id)∗)? ;
-term ::= \old ( term ) | \result | \nothing | \everything
+term ::= \old ( term ) | \result | \nothing | ...
 pred ::= \old ( pred )
 }}}
@@ -64 +64 @@
 [[* `mem1+mem2`, where `mem1` and `mem2` are expressions of type `$memory`.  This is the union of the two sets.]]  Problem this is ambiguous with numeric +, as in x+y.
 
-== `assigns` clause ==
+== `assigns` and `reads` clause ==
 
 As in other contract specification language, this contract clause is used to specify a set of existing memory units.    The claim is that if an existing memory unit is not in the set, it will not be modified in the course of the function call.  The syntax is:
 
-`assigns location (, location)*` or `assigns \nothing` or `assigns $everything`
+`assigns/reads location (, location)*` or `assigns/reads \nothing`
 
 where `location` is a `tset` expressions of type `$memory`.
@@ -77 +77 @@
 }}}
 
+* absence of `assigns`/`reads` clause
+ * for non-system functions, the function body is scanned to understand the memory locations assigned/read by it
+ * for system functions, only memory locations reachable form the arguments shall be assigned/read
 
 == `depends` clause ==