Changes between Version 23 and Version 24 of ContractReduction

Timestamp:

12/07/15 11:38:07 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -1 +1 @@
 == Contract Reduction Language  ==
+
+== ACSL function contract grammar with CIVL-C extension (in bold) ==
+
+`function-contract ::= requires-clause∗ terminates-clause? decreases-clause?`
+                                 `simple-clause∗ named-behavior∗ completeness-clause∗`
+
+`requires-clause ::= requires pred ;`
+
+`terminates-clause ::= terminates pred ;`
+
+`decreases-clause  ::= decreases term (for id)? ;`
+
+`simple-clause ::= assigns-clause | ensures-clause | allocation-clause | abrupt-clause-fn`
+
+`assigns-clause ::= assigns locations ;`
+
+`locations ::= location (, location) ∗ | \nothing |` **\everything**
+
+`location ::= tset`
+
+`ensures-clause ::= ensures pred ;`
+
+`named-behavior ::= behavior id : behavior-body`
+
+`behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗`
+
+`assumes-clause ::= assumes pred ;`
+
+`completeness-clause ::= complete behaviors (id (, id)∗)? ;`
+                      `| disjoint behaviors (id (, id)∗)? ;`
+
+{{{
+tset ::= \empty
+       | tset -> id 
+       | tset . id * tset
+       | & tset
+       | tset [ tset ]
+       | term? .. term?
+       | \union ( tset (, tset)∗ )
+       | \inter ( tset (, tset)∗ )
+       | tset + tset
+       | ( tset )
+       | { tset | binders (; pred)? }
+       | { term } term
+}}}
+
+`term ::= \old ( term ) | \result`
+
+`pred ::= \old ( pred )`
 
 
 == `$memory` type ==
 
-The new built-in type `$memory` denotes a set of memory units.  The following expressions have type `$memory`:
+The new built-in type `$memory` denotes a set of memory units (aka., memory locations).  The following expressions have type `$memory`:
 * a left-hand-side expression, when used in certain contexts, is automatically converted to `$memory`.  The contexts are: arguments to the built-in functions `$access`, `$read`, and `$write` described below, or occurrence in the list of an `$assigns` clause
 * `a[dom]`, where `a` is an expression of array type and `dom` is an expression of `$domain` type.   The dimension of the array must match the dimension of the domain.   This represents all memory units which are the cells in the array indexed by a tuple in `dom`.
@@ -11 +60 @@
 [[* `mem1+mem2`, where `mem1` and `mem2` are expressions of type `$memory`.  This is the union of the two sets.]]  Problem this is ambiguous with numeric +, as in x+y.
 
-== `$assigns` clause ==
+== `assigns` clause ==
 
 As in other contract specification language, this contract clause is used to specify a set of existing memory units.    The claim is that if an existing memory unit is not in the set, it will not be modified in the course of the function call.  The syntax is:
-{{{
-$assigns {<memory-list>}
-}}}
+`assigns location (, location)*` or `assigns \nothing`
+
 where `<memory-list>` is a comma-separated list of expressions of type `$memory`.
 
 Example:
 {{{
-$assigns x,a[i][j],$region(list->head),b[dom];
+assigns x,a[i][j],$region(list->head),b[dom];
 }}}