Changes between Initial Version and Version 1 of Function_Contracts

Timestamp:

01/11/16 16:31:27 (10 years ago)

Author:

zmanchun

Comment:

--

Function_Contracts

@@ +1 @@
+== 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`
+* simple clauses:
+ * `ensures e;`
+ * `assumes e;`
+ * `assigns e0, e1, ...;`
+ * `allocates e0, e1, ...;`
+ * `frees e0, e1, ...;`
+ * `guards e;`
+ * `reads e0, e1, ...;`
+ * `depends e0, e1, ...;`
+
+* action expressions:
+ * `read(e)`: `e` has type `Mem`. The function reads the memory units specified by `e`.
+ * `write(e)`: `e` has type `Mem`. The function writes the memory units specified by `e`.
+ * `call(f, <e1, ...>)`: `f` has type `Function`. The function calls `f` with parameters `e1, ...`.
+ * `noaction`: no action
+ * `anyaction`: all actions
+ * `act_union(ma0, ma1)`: the union of the two memory set actions `ma0` and `ma1`.
+ * `act_comp(ma0, ma1)`: action complement (everything not in `ma1`)
+ * `act_isect(ma0, ma1)`: action intersection
+
+* depends clause: `depends action0, action1, action2, ... `
+ * Example: `depends act_union(act_comp(read(n), call(inc, <x>))), call(dec, <y>))`
+ * absence of depends clause: there is no information about the dependency of the function, which means that the analysis needs to figure it out by itself.
+* some facts about assigns-or-reads clause
+ * absence of `reads`/`assigns` clause: there is no assumption about the read/assign access of the function, i.e., the function could read/assign anything
+  * absence of `assigns` clause: similar to the absence of `reads` clause
+ * `reads/assigns nothing` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body. **check it**
+
+* For an independent function which has `depends coaction`, usually we also need to specify `reads nothing`, for the purpose of reachability analysis.
+e.g., 
+{{{
+/* Returns the size of the given bundle b. */
+bundle_size(Bundle b): Integer
+  depends nothing
+  reads b
+  ;
+}}}
+
+* Example of a function declaration with contracts: 
+{{{
+fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
+  reads deref(buf);
+  behavior send:
+    depends writes(buf);
+    assigns nothing;
+  behavior receive:
+    depends access(deref(buf));
+    assigns deref(buf);
+{
+  begin choose
+  when eq(cmd, 0)
+     do CALL send, <buf, ...>; goto L1;
+  when eq(cmd, 1)
+    do CALL recv, <buf, ...>; goto L1;
+  when and(neq(cmd, 0), neq(cmd, 1))
+    do NOOP; goto L1;
+  end choose
+L1:
+}
+}}}