Changes between Version 12 and Version 13 of ContractReduction

Timestamp:

07/21/14 11:36:39 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -35 +35 @@
 The following built-in functions may be used as constituents in the boolean expression `e`:
 
-* `_Bool $access($memory mem)`
- * holds if any memory unit in `mem` may be read or modified by `p` at some point now or in the future.
-* `_Bool $write($memory mem)`
- * holds if any memory unit in `mem` may be modified by `p` at some point now or in the future.
-* `_Bool $read($memory mem)`
- * holds if any memory unit in `mem` may be read by `p` at some point now or in the future.
+* `_Bool $access(<memory-list>)`
+ * holds if any memory unit in the list may be read or modified by `p` at some point now or in the future.
+* `_Bool $write(<memory-list>)`
+ * holds if any memory unit in the list may be modified by `p` at some point now or in the future.
+* `_Bool $read(<memory-list>)`
+ * holds if any memory unit in the list may be read by `p` at some point now or in the future.
 
 Default: if there is no `$depends` clause present:
@@ -50 +50 @@
 Both `$atomic` and `$atom` may be used as function specifiers.   They designate that any call to the function is to be treated atomically or atom-ly, respectively.
 
-
-
-===  Examples ===
+==  Examples ==
 
 - The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set.