7.3. Coroutine rely/guarantee contracts🔗

Because a coroutine is suspended across a yield, the environment may act in between. The relies and guarantees clauses specify that boundary, and are checked at every yield:

• A guarantees G clause states a property the coroutine establishes at each yield (and when it halts). It is asserted there.

• A relies R clause states a property the coroutine may assume the environment maintained across the suspension. It is assumed on entry and after each yield.

Both may be two-state: old(e) inside a clause refers to the state at the start of the coroutine's current step. The example below verifies: the coroutine relies on the environment never decreasing the shared counter, and guarantees that its own step strictly increases it.

composite Cell { var x: int }

coroutine incMonotonic(s: Cell)
  requires s#x == 0
  relies old(s#x) <= s#x
  guarantees old(s#x) < s#x
  modifies s
{
  while (true)
      invariant oldGuarantee(s#x) <= s#x
  {
    s#x := s#x + 1;
    yield
  }
};

Inside a loop that contains a yield, the per-yield guarantee is not threaded through the loop head automatically: write the loop invariant explicitly using oldGuarantee(e), which refers to the state at the start of the current step (as old(e) does inside a guarantees clause). The invariant above restates the guarantee's baseline so the next iteration's yield can discharge it.