Changes between Version 26 and Version 27 of ContractReduction

Timestamp:

12/07/15 11:54:45 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -10 +10 @@
 simple-clause ::= assigns-clause | ensures-clause 
                 | allocation-clause | abrupt-clause-fn
-                | depends-clause
+                | reads-clause | depends-clause
 assigns-clause ::= assigns locations ;
 locations ::= location (, location) ∗ | \nothing | $everything
 location ::= tset
 ensures-clause ::= ensures pred ;
+reads-clause ::= $reads locations;
 depends-clause := $depends event (, event)*;
 named-behavior ::= behavior id : behavior-body