== Contract Reduction Language  ==

== `$depend` clause ==

The following contractual clause may appear in a function contract in the same places that `$ensures` or `$requires` clauses can appear:
{{{
$depends e ;
}}}
where `e` is an expression of boolean type.   For each process `p`, the `e` can be evaluated in the context of `p`.   If `e` evaluates to `true`, then `p` must be included in an ample set containing a call to this function. 

The following boolean expressions may be used as constituents in the boolean expression `e`:

* `$access(void * obj)`
 * holds iff the memory unit pointed to by `obj` is reachable from `p`.  This means there is a path from the variables on the call stack of `p` to the memory unit, following array elements, struct members, and pointer dereferences, pointer arithmetic.
* `$accessRegion(void * obj)`
 * holds iff any of the memory units reachable from `obj` (including the object pointed to by `obj` itself) is reachable from`p`
* `$write(void * obj)`
 * holds iff the memory unit pointed to by `obj` is not only reachable from `p` but if it is possible that `p` (or a process spawned by `p`) could write to that memory unit at some point now or in the future.
* `$writeRegion(void * obj)`
 * like above but true if any of the memory units in the reachable region specified by `obj` may be written to


* Things to be decided:
   - what shall DEFAULT (when the `$depend` expression is absent) do?
   - how to specify the case when we need the library enabler to decide the ample set?
   - what keyword to use to specify functions to execute as one step, `$atomic`, `_Atomic`, etc.

===  Examples ===

- The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
{{{
void comm_deque($comm comm, ....)
  $depend $access(void * obj);
;
}}}

- The following means that any process that can reach any of the memory units reachable from `a` or write any of the memory units reachable from `a` now or in the future should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
{{{
void strcpy(char *a, char *b)
  $depend $accessRegion(a) || $writeRegion(b);
;
}}}

- The following means that the current process itself can form the ample set.
{{{
int $comm_size($comm, ...)
  $depend $false;
;
}}}

- The following means that if the argument `count` is equal to zero, then the current process forms the ample set, otherwise, any process that can reach the memory unit of object `comm` should be in the ample set.
{{{
void comm_deque($comm comm, int count ....)
  $depend count==0 ? $false : $access(comm);
;
}}}