blob: b572996e2f12d982c1a88799314d89b470c9b711 (
plain) (
blame)
1
2
3
4
|
This module implements a deterministic, rectifying variant on Dijkstra's
guarded commands. Each named step is passed two blocks: an "ensure"
block that defines a test for a necessary and sufficient condition of
the step, and a "using" block that will cause that condition to obtain.
|