Changes between Version 41 and Version 42 of ContractReduction

Timestamp:

12/14/15 10:30:48 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -5 +5 @@
 * `guards` clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body
 * `depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
- * `\calls(fun, arg0, arg1, ...)`: an action of invoking a function with certain arguments
- * `\noact`: empty set of actions ** or `depends false`?**
- * `\anyact`: any actions ** or `depends true`?**
- * memory actions: `\read(mu-list)`, `\write(mu-list)`
- * action operations: `+`, `-`, `&`
+ * `\calls(fun, arg0, arg1, ...)`: a set of actions that invokes the function with the specified arguments
+ * `\noact`: empty set of actions 
+ * `\anyact`: any action sets 
+ * set of memory actions: `\read(mu-list)`, `\write(mu-list)`
+ * action set operations: `+` union, `-` complement, `&` intersect
 * `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 `$root` is used
+* additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope is used
 
 {{{