Changes between Version 4 and Version 5 of ContractReduction

Timestamp:

07/01/14 15:22:23 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -1 +1 @@
 == Contract Reduction Language  ==
 
-Given a process `p` that is at a state that a call to a system function `f` is enabled,
-if `p` is chosen in the ample set, then the following represents the set of processes other than
-`p` that have to be in the ample set as well:
+The following contractual clause may appear in a function contract in the same places that `$ensures` or `$requires` clauses can appear:
+{{{
+$depends expr ;
+}}}
+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`.
 
-`$ample{ BOOLEAN EXPRESSION }`
+The following boolean expressions may be used as constituents in the boolean expression `e`:
 
-    where `BOOLEAN EXPRESSION` is composed of the following functions over `f`'s arguments (`a, ...`).
+- `$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(a, ...)`
-    returns true iff the memory unit of the object `a` (or others if present) is reachable by a given process `p'`.
+- `$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'`.
 
-- `$reach_from(a, ...)`
-    returns true iff any of the memory units reachable from the object `a` (or others if present) is reachable by a given 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(a, ...)`
-    returns true iff the memory unit of the object `a` (or others if present) is to be written now or in the future by a given process `p'`.
+- `$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
 
-- `$write_from(a, ...)`
-    returns true iff any of the memory units reachable from the object `a` (or others if present) is to be written now or in the future by a given process `p'`.
-
-- `$ample{$true}`
-    any process exists in the state should be in the ample set
-
-- `$ample{$false}`
-    any process other than the current process (`$self`) need NOT be in the ample set.
 
 Conditional amples set: `[COND] $ample{EXPR1} : $ample(EXPR2)`