Changes between Version 21 and Version 22 of ContractReduction

Timestamp:

05/01/15 11:52:17 (11 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -15 +15 @@
 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 <memory-list>;
+$assigns {<memory-list>}
 }}}
 where `<memory-list>` is a comma-separated list of expressions of type `$memory`.
@@ -29 +29 @@
 This contractual clause specifies part of the dependence relation used in POR.
 {{{
-$depends e ;
+$depends {e}
 }}}
 where `e` is an expression of boolean type.   For each process `p`, the `e` can be evaluated in the context of `p`.   If `e` evaluates to `true`, then `p` must be included in an ample set containing a call to this function. 
@@ -132 +132 @@
 
 {{{
-$guard <bool-expr> ;
+$guard {<bool-expr>}
 }}}