class
Std.Internal.Do.WPConjunctive
{Prog : Type u}
{Value : outParam (Type v)}
{Pred : outParam (Type w)}
{EPred : outParam (Type z)}
[Assertion Pred]
[Assertion EPred]
[WP Prog Value Pred EPred]
(x : Prog)
:
wp x is sub-conjunctive: a meet of postconditions maps below the wp of their meet. A
healthiness condition of the WP interpretation for the individual program x; it holds for the base
interpretations and lifts through the transformers.
- wp_meet_wp_le (Q₁ Q₂ : Value → Pred) (E₁ E₂ : EPred) : Lean.Order.PartialOrder.rel (Lean.Order.meet (wp x Q₁ E₁) (wp x Q₂ E₂)) (wp x (Lean.Order.meet Q₁ Q₂) (Lean.Order.meet E₁ E₂))
A meet of postconditions maps below the
wpof their meet.
Instances
An Id program is conjunctive: its wp is evaluation at the result.
An Option program is conjunctive: its wp is evaluation at the result.
An Except ε program is conjunctive: its wp is evaluation at the result.
An EStateM program is conjunctive: its wp is evaluation at the result.
instance
Std.Internal.Do.StateT.instWPConjunctive
{m : Type u → Type v}
{σ : Type u}
{Pred : Type w}
{EPred : Type z}
{α : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
(x : StateT σ m α)
[base : ∀ (s : σ), WPConjunctive (x.run s)]
:
A StateT program lifts conjunctivity from its base monad.
instance
Std.Internal.Do.ReaderT.instWPConjunctive
{m : Type u → Type v}
{ρ : Type u}
{Pred : Type w}
{EPred : Type z}
{α : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
(x : ReaderT ρ m α)
[base : ∀ (r : ρ), WPConjunctive (x.run r)]
:
A ReaderT program lifts conjunctivity from its base monad.