Changes between Version 25 and Version 26 of ContractReduction

Timestamp:

12/07/15 11:52:43 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -1 +1 @@
 == Contract Reduction Language  ==
 
-== ACSL function contract grammar with CIVL-C extension (in bold) ==
+== ACSL function contract grammar with CIVL-C extension (starting with `$`) ==
 {{{
 function-contract ::= requires-clause∗ terminates-clause? decreases-clause?
-                      simple-clause∗ named-behavior∗ completeness-clause∗
+                      simple-clause∗  named-behavior∗ completeness-clause∗ 
 requires-clause ::= requires pred ;
 terminates-clause ::= terminates pred ;
@@ -10 +10 @@
 simple-clause ::= assigns-clause | ensures-clause 
                 | allocation-clause | abrupt-clause-fn
+                | depends-clause
 assigns-clause ::= assigns locations ;
-locations ::= location (, location) ∗ | \nothing |` $everything
+locations ::= location (, location) ∗ | \nothing | $everything
 location ::= tset
 ensures-clause ::= ensures pred ;
+depends-clause := $depends event (, event)*;
 named-behavior ::= behavior id : behavior-body
 behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗
@@ -70 +72 @@
 where `event` is a memory event represented as a boolean expression.   For each process `p`, the `event ` can be evaluated in the context of `p`.   If `event ` evaluates to `true`, then `p` must be included in an ample set containing a call to this function. 
 
-The expression `e` hence defines a predicate d(s,p), where s ranges over states, and p over procs.   The requirement is the following:
+The expression `event ` hence defines a predicate d(s,p), where s ranges over states, and p over procs.   The requirement is the following:
 
 Let s be any state and p a proc such that a function call for this function is enabled in p.  Then in any execution departing from s, no transition dependent on the execution of this function call can occur without a transition from p or a proc q satisfying d(s,q) occurring first.