Changes between Version 30 and Version 31 of ContractReduction

Timestamp:

12/07/15 14:04:48 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -17 +17 @@
                 | allocation-clause | abrupt-clause-fn
                 | reads-clause | depends-clause
-assigns-clause ::= assigns locations ;
-locations ::= location (, location) ∗ | \nothing | $everything
-location ::= tset
+assigns-clause ::= assigns tsets ;
+tsets ::= location (, location) ∗
 ensures-clause ::= ensures pred ;
-allocation-clause ::= allocates dyn-allocation-addresses ; | frees dyn-allocation-addresses ;
-dyn-allocation-addresses ::= location-addresses | \nothing
-reads-clause ::= $reads locations;
+allocation-clause ::= allocates tsets ; | frees tsets ;
+reads-clause ::= $reads tsets;
 depends-clause := $depends event (, event)*;
 named-behavior ::= behavior id : behavior-body
@@ -30 +28 @@
 completeness-clause ::= complete behaviors (id (, id)∗)? ;
                       | disjoint behaviors (id (, id)∗)? ;
-term ::= \old ( term ) | \result
+term ::= \old ( term ) | \result | \nothing | $everything
 pred ::= \old ( pred )
 }}}