== 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 expr ;
}}}
where `expr` is an expression of type function-from-`$proc`-to-boolean.  This expression will usually be specified as a lambda expression:
{{{
$depends $lambda($proc p) e ;
}}}
where `e` is a boolean expression, usually involving `p`.

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

- `$reach($proc p, void * obj)`
    returns true iff the memory unit pointed to by `obj` is reachable from process `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($proc p, void * obj)`
    returns true 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 process `p'`.

- `$write($proc p, void * obj)`
    returns true 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($proc p, 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 ....);
}}}