| #
5deb58a9 |
|
23-May-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: add the Interference Trace Monad.
Adds another style of monad to the existing ones in lib/Monad_WP.
The Interference Trace monad is an extension of the nondeterministic
state monad to record interactions between the task and its environment.
It supports a parallel composition operator.
The VCG for this monad includes the same Hoare triple style as for the
state monads, and also includes a rely-guarantee quintuple which can be
used to verify a parallel composition of programs.
|