Weakest precondition interpretation #
This module defines the weakest precondition interpretation WP
of monadic programs
in terms of predicate transformers PredTrans
.
This interpretation forms the basis of our notion of Hoare triples. It is the main mechanism of this library for reasoning about monadic programs.
An instance WP m ps
determines an interpretation wp⟦x⟧
of a program x : m α
in terms of a
predicate transformer PredTrans ps α
; The monad m
determines ps : PostShape
and hence
the particular shape of the predicate transformer.
This library comes with pre-defined instances for common monads and transformers such as
WP Id .pure
, interpreting pure computationsx : Id α
in terms of a function (isomorphic to)(α → Prop) → Prop
.WP (StateT σ m) (.arg σ ps)
given an instanceWP m ps
, interpretingStateM σ α
in terms of a function(α → σ → Prop) → σ → Prop
.WP (ExceptT ε m) (.except ε ps)
given an instanceWP m ps
, interpretingExcept ε α
in terms of(α → Prop) → (ε → Prop) → Prop
.WP (EStateM ε σ) (.except ε (.arg σ .pure))
interpretsEStateM ε σ α
in terms of a function(α → σ → Prop) → (ε → σ → Prop) → σ → Prop
.
These instances are all monad morphisms, a fact which is properly encoded and exploited
by the subclass WPMonad
.
A weakest precondition interpretation of a monadic program x : m α
in terms of a
predicate transformer PredTrans ps α
.
The monad m
determines ps : PostShape
. See the module comment for more details.
Instances
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Std.Do.Id.instWP = { wp := fun {α : Type} (x : Id α) => Std.Do.PredTrans.pure x.run }
Equations
- Std.Do.StateT.instWP = { wp := fun {α : Type} (x : StateT σ m α) => Std.Do.PredTrans.pushArg fun (s : σ) => Std.Do.wp (x s) }
Equations
- Std.Do.ExceptT.instWP = { wp := fun {α : Type} (x : ExceptT ε m α) => Std.Do.PredTrans.pushExcept (Std.Do.wp x) }
Equations
- One or more equations did not get rendered due to their size.