== Contract Reduction Language  ==

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

* `$reach(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 following array elements, struct members, and pointer dereferences.
* `$reach_rec(void * obj)`
 * holds iff any of the memory units reachable from the object pointed to by `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.
* `$write_rec(void * obj)`
 * like above but true if any of the memory units in the reachable region specified by `obj` may be written to


Conditional amples set: `[COND] $ample{EXPR1} : $ample(EXPR2)`
    if `COND` is satisfied then processes satisfying `EXPR1` should be in the ample set;
    otherwise, `EXPR2` is considered.

Absent ample set (DEFAULT case): if no `$ample` expression is present, then the library enabler needs to calculate the ample set.

   
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.
{{{
$ample{$reach(comm)}
void comm_deque($comm comm, ....);
}}}

- 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.
{{{
$ample{$reach_from(a) || $write_from(b)}
void strcpy(char *a, char *b);
}}}

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

- 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.
{{{
[count = 0] $ample{$false} : $ample{$reach(comm)}
void comm_deque($comm comm, int count ....);
}}}