This PR allows gates of atomic actions to be explicitly specified. The convention is as follows:
var {:layer 0,1} x: int;
yield invariant YieldInv();
invariant ...
atomic action Foo()
requires x > 0; // gate (must be sufficient to prove absence of failures in atomic action)
requires call YieldInv(); // precondition used only in special circumstances
{
assert x != 0;
}
This PR allows gates of atomic actions to be explicitly specified. The convention is as follows:
var {:layer 0,1} x: int;
yield invariant YieldInv(); invariant ...
atomic action Foo() requires x > 0; // gate (must be sufficient to prove absence of failures in atomic action) requires call YieldInv(); // precondition used only in special circumstances { assert x != 0; }