Changes between Version 13 and Version 14 of ContractReduction

Timestamp:

07/21/14 11:57:24 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -42 +42 @@
  * 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:
-* if the body of the function is not provided, i.e., the function is a system function, the verifier will assume that execution of the function may read and/or modify any memory unit that it can reach, and decide on the partial order reduction appropriately
+Default: if there is no `$depends` clause present, the dependency information will be obtained from Java code in the library enabler.  If the library enabler does not specify anything for this function, the default rules will be used, which are sound:
+* if the body of the function is not provided, i.e., the function is a system function, the verifier will assume that execution of the function may read and/or modify any memory unit that it can reach, and decide on the partial order reduction appropriately, else
 * if the body of the function is present, the statements comprising the body may be analyzed to further restrict the reduction.
 
@@ -49 +49 @@
 
 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.
+
+== Guards ==
+
+The following construct is used to specify a guard for a function.  The function may be a system or ordinary function.  It maybe used in conjunction with `$atom` or `$atomic`.
+Grammatically, it is a contract clause, though it is not really part of the contract.  
+
+{{{
+$guard <bool-expr> ;
+}}}
+
+If missing, the default is to go the library enabler for the guard.  If the library enabler does not specify a guard, it defaults to `$true`.
 
 ==  Examples ==