Changes between Version 1 and Version 2 of Function_Contracts

Timestamp:

01/11/16 16:53:24 (10 years ago)

Author:

zmanchun

Comment:

--

Function_Contracts

@@ +1 @@
+The contracts specification of CIVL-C is based on ACSL, with additional primitives and constructs for various purposes, such as function guard, function dependency, MPI function behavior, etc.
+
+== overview ==
+The grammar for the contract specification of a function is as follows:
+
+{{{
+contract: requires* terminates? decreases? simple* behavior* completeness* ;
+requires: 'Requires' e ';' ;
+...
+simple: ensures | assumes | assigns | reads | guards | depends | ... ;
+ensures: 'Ensures' e ';' ;
+assumes: 'Assumes' e ';' ;
+assigns: 'Assigns' e (',' e)* ';' ;
+reads: 'Reads' e (',' e)* ';' ;
+depends: 'Depends' e (',' e)* ';' ;
+...
+behavior: 'Behavior' id ':' behaviorBody ;
+behaviorBody: behaviorClause+;
+behaviorClause: assumes | requires | simple ;
+completeness: 'Complete' (id (',' id)*)? 
+            | 'Disjoint' (id (',' id)*)? 
+            ;
+}}}
+
 == contract clauses ==
 
-* `requires e;`: precondition, `e` should hold at the entry of the function
-* `terminates e;`: 
-* `decreases e ;` or `decreases e for r`;: decreases clause, where `e` is an expression of type `T` and `r` is an relation over `T`
+* `Requires e;`: precondition, `e` has `Bool` type and should hold at the entry of the function
+* `Terminates e;`: `e` has `Bool` type and if `e` holds then the function should terminate eventually
+* `Decreases e ;` or `Decreases e for r`;: decreases clause, where `e` is an expression of type `T` and `r` is an relation over `T`
 * simple clauses:
- * `ensures e;`
- * `assumes e;`
- * `assigns e0, e1, ...;`
- * `allocates e0, e1, ...;`
- * `frees e0, e1, ...;`
- * `guards e;`
- * `reads e0, e1, ...;`
- * `depends e0, e1, ...;`
+ * `Ensures e;`: postcondition, `e` has `Bool` type and should hold when the function terminates
+ * `Assumes e;`: assumption, `e` has `Bool` type
+ * `Assigns e0, e1, ...;`: side-effects, `e0, e1, ...` have `Mem` type
+  * absence of `Assigns` clause does NOT mean that the function has no side-effects
+  * `Assigns \nothing`: means that the function has no side-effects
+ * `Allocates e0, e1, ...;`: memory units allocated by the function, `e0, e1, ...` have `Mem` type
+ * `Frees e0, e1, ...;`: memory units deallocated by the function, `e0, e1, ...` have `Mem` type
+ * `Guards e;`: guard of the function, where `e` has `Bool` type
+ * `Reads e0, e1, ...;`: memory access, where `e0, e1, ...` have `Mem` type
+  * similar to `Assigns`
+  * absence of `Reads` clause does NOT mean that the function does NOT read anything
+  * `Reads \nothing`: means that the function does NOT read the memory
+ * `Depends e0, e1, ...;`: dependency relation, where `e0, e1, ...` have `Mem` type
+ * Note: `Guards`, `Depends` and `Reads` are CIVL extension for ACSL
 
 * action expressions: