Changes between Version 5 and Version 6 of ContractReduction

Timestamp:

07/01/14 22:30:31 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -3 +3 @@
 The following contractual clause may appear in a function contract in the same places that `$ensures` or `$requires` clauses can appear:
 {{{
-$depends expr ;
+$depends e ;
 }}}
-where `expr` is an expression of type function-from-`$proc`-to-boolean.  This expression will usually be specified as a lambda expression:
-{{{
-$depends $lambda($proc p) e ;
-}}}
-where `e` is a boolean expression, usually involving `p`.
+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. 
 
 The following boolean expressions may be used as constituents in the boolean expression `e`:
 
-- `$reach($proc p, void * obj)`
-    returns true iff the memory unit pointed to by `obj` is reachable from process `p`.  This means there is a path from the variables on the call stack of `p` to the memory unit, following following array elements, struct members, and pointer dereferences.
-
-- `$reach_rec($proc p, void * obj)`
-    returns true iff any of the memory units reachable from the object pointed to by obj (including the object pointed to by `obj` itself) is reachable from process `p'`.
-
-- `$write($proc p, void * obj)`
-    returns true iff the memory unit pointed to by `obj` is not only reachable from `p` but if it is possible that `p` (or a process spawned by `p`) could write to that memory unit at some point now or in the future.
-
-- `$write_rec($proc p, void * obj)`
-    like above but true if any of the memory units in the reachable region specified by `obj` may be written to
+* `$reach(void * obj)`
+ * holds iff the memory unit pointed to by `obj` is reachable from `p`.  This means there is a path from the variables on the call stack of `p` to the memory unit, following following array elements, struct members, and pointer dereferences.
+* `$reach_rec(void * obj)`
+ * holds iff any of the memory units reachable from the object pointed to by `obj` (including the object pointed to by `obj` itself) is reachable from`p`
+* `$write(void * obj)`
+ * holds iff the memory unit pointed to by `obj` is not only reachable from `p` but if it is possible that `p` (or a process spawned by `p`) could write to that memory unit at some point now or in the future.
+* `$write_rec(void * obj)`
+ * like above but true if any of the memory units in the reachable region specified by `obj` may be written to