Changes between Version 4 and Version 5 of Function_Contracts

Timestamp:

01/11/16 17:30:47 (10 years ago)

Author:

zmanchun

Comment:

--

Function_Contracts

@@ -44 +44 @@
 L1:
 }
-
 }}}
 
@@ -67 +66 @@
  * `Depends e0, e1, ...;`: dependency relation, where `e0, e1, ...` have `Mem` type
  * Note: `Guards`, `Depends` and `Reads` are CIVL extension for ACSL
+* named behavior:
+ * `Behavior id : c0; c1; c2; ...`, where `id` is the name of this behavior, `c0, c1, c2, ...` are behavior clauses
+ * behavior clause: a clause that can be used in the body of a behavior, and could be one of the following:
+  * assumes clause
+  * requires clause
+  * simple clause
+* completeness clause
+ * `Complete;` or `Complete (id0, id1, ...);`: 
+ * `Disjoint;` or `Disjoint (id0, id1, ...);`
+
+== depends clause and actions ==
 
 * action expressions: