Changes between Version 2 and Version 3 of ContractReduction

Timestamp:

06/30/14 09:56:20 (12 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -10 +10 @@
 
 - `$reach(a, ...)`
-    returns true iff the memory unit of the object `a` (and others if present) is reachable by a given process `p'`.
+    returns true iff the memory unit of the object `a` (or others if present) is reachable by a given process `p'`.
 
 - `$reach_from(a, ...)`
-    returns true iff any of the memory units reachable from the object `a` (and others if present) is reachable by a given process `p'`.
+    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(a, ...)`
-    returns true iff the memory unit of the object `a` (and others if present) is to be written now or in the future by a given process `p'`.
+    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_from(a, ...)`
-    returns true iff any of the memory units reachable from the object `a` (and others if present) is to be written now or in the future by a given process `p'`.
+    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}`