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:
  }