lib+READMEs: rename Monad_WP to Monads
In preparation for a separate Monads session. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
34c427d09d
commit
bba173cb99
46
lib/ROOT
46
lib/ROOT
|
@ -12,8 +12,8 @@ session Lib (lib) = Word_Lib +
|
||||||
Eisbach_Tools
|
Eisbach_Tools
|
||||||
ML_Utils
|
ML_Utils
|
||||||
directories
|
directories
|
||||||
"Monad_WP"
|
"Monads"
|
||||||
"Monad_WP/wp"
|
"Monads/wp"
|
||||||
theories
|
theories
|
||||||
Lib
|
Lib
|
||||||
AddUpdSimps
|
AddUpdSimps
|
||||||
|
@ -74,27 +74,27 @@ session Lib (lib) = Word_Lib +
|
||||||
|
|
||||||
(* should really be a separate session, but too entangled atm: *)
|
(* should really be a separate session, but too entangled atm: *)
|
||||||
NonDetMonadLemmaBucket
|
NonDetMonadLemmaBucket
|
||||||
"Monad_WP/WhileLoopRules"
|
"Monads/WhileLoopRules"
|
||||||
"Monad_WP/TraceMonad"
|
"Monads/TraceMonad"
|
||||||
"Monad_WP/OptionMonadND"
|
"Monads/OptionMonadND"
|
||||||
"Monad_WP/OptionMonadWP"
|
"Monads/OptionMonadWP"
|
||||||
"Monad_WP/Strengthen_Demo"
|
"Monads/Strengthen_Demo"
|
||||||
"Monad_WP/TraceMonadLemmas"
|
"Monads/TraceMonadLemmas"
|
||||||
"Monad_WP/wp/WPBang"
|
"Monads/wp/WPBang"
|
||||||
"Monad_WP/wp/WPFix"
|
"Monads/wp/WPFix"
|
||||||
"Monad_WP/wp/Eisbach_WP"
|
"Monads/wp/Eisbach_WP"
|
||||||
"Monad_WP/wp/WPI"
|
"Monads/wp/WPI"
|
||||||
"Monad_WP/wp/WPC"
|
"Monads/wp/WPC"
|
||||||
"Monad_WP/wp/WP_Pre"
|
"Monads/wp/WP_Pre"
|
||||||
"Monad_WP/wp/WP"
|
"Monads/wp/WP"
|
||||||
"Monad_WP/Datatype_Schematic"
|
"Monads/Datatype_Schematic"
|
||||||
"Monad_WP/WhileLoopRulesCompleteness"
|
"Monads/WhileLoopRulesCompleteness"
|
||||||
"Monad_WP/Strengthen"
|
"Monads/Strengthen"
|
||||||
"Monad_WP/OptionMonad"
|
"Monads/OptionMonad"
|
||||||
"Monad_WP/TraceMonadVCG"
|
"Monads/TraceMonadVCG"
|
||||||
"Monad_WP/NonDetMonadVCG"
|
"Monads/NonDetMonadVCG"
|
||||||
"Monad_WP/NonDetMonad"
|
"Monads/NonDetMonad"
|
||||||
"Monad_WP/NonDetMonadLemmas"
|
"Monads/NonDetMonadLemmas"
|
||||||
|
|
||||||
session CLib (lib) in clib = CParser +
|
session CLib (lib) in clib = CParser +
|
||||||
sessions
|
sessions
|
||||||
|
|
|
@ -9,7 +9,7 @@ Abstract Spec Invariant Proof
|
||||||
|
|
||||||
This proof defines and proves the global invariants of seL4's
|
This proof defines and proves the global invariants of seL4's
|
||||||
[abstract specification](../../spec/abstract/). The invariants are
|
[abstract specification](../../spec/abstract/). The invariants are
|
||||||
phrased and proved using a [monadic Hoare logic](../../lib/Monad_WP/NonDetMonad.thy)
|
phrased and proved using a [monadic Hoare logic](../../lib/Monads/NonDetMonad.thy)
|
||||||
described in a TPHOLS '08 [paper][1].
|
described in a TPHOLS '08 [paper][1].
|
||||||
|
|
||||||
[1]: https://trustworthy.systems/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"
|
[1]: https://trustworthy.systems/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"
|
||||||
|
|
|
@ -14,7 +14,7 @@ specification. The specification draws in additional interface files from
|
||||||
`design` and `machine`.
|
`design` and `machine`.
|
||||||
|
|
||||||
The specification is written in monadic style. See
|
The specification is written in monadic style. See
|
||||||
`l4v/lib/Monad_WP/NonDetMonad` for the definition of this monad.
|
`l4v/lib/Monads/NonDetMonad` for the definition of this monad.
|
||||||
|
|
||||||
Top-Level Theory
|
Top-Level Theory
|
||||||
----------------
|
----------------
|
||||||
|
|
Loading…
Reference in New Issue