Predicate transformers for arbitrary postcondition shapes #
This module defines the type PredTrans ps
of predicate transformers for a given ps : PostShape
.
PredTrans
forms the semantic domain of the weakest precondition interpretation
WP
in which we interpret monadic programs.
A predicate transformer x : PredTrans ps α
is a function that takes a postcondition
Q : PostCond α ps
and returns a precondition x.apply Q : Assertion ps
, with the additional
monotonicity property that the precondition is stronger the stronger the postcondition is:
Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂
.
Since PredTrans
itself forms a monad, we can interpret monadic programs by writing
a monad morphism into PredTrans
; this is exactly what WP
encodes.
This module defines interpretations of common monadic operations, such as get
, throw
,
liftM
, etc.
The stronger the postcondition, the stronger the transformed precondition.
Equations
- Std.Do.PredTrans.Monotonic t = ∀ (Q₁ Q₂ : Std.Do.PostCond α ps), (Q₁ ⊢ₚ Q₂) → t Q₁ ⊢ₛ t Q₂
Instances For
Transforming a conjunction of postconditions is the same as the conjunction of transformed postconditions.
Equations
- Std.Do.PredTrans.Conjunctive t = ∀ (Q₁ Q₂ : Std.Do.PostCond α ps), t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂
Instances For
Any predicate transformer that is conjunctive is also monotonic.
Equations
- ⋯ = ⋯
Instances For
The type of predicate transformers for a given ps : PostShape
and return type α : Type
.
A predicate transformer x : PredTrans ps α
is a function that takes a postcondition
Q : PostCond α ps
and returns a precondition x.apply Q : Assertion ps
, with the additional
monotonicity property that the precondition is stronger the stronger the postcondition is:
Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂
.
- conjunctive : Conjunctive self.apply
Instances For
Equations
Equations
- Std.Do.PredTrans.pure a = { apply := fun (Q : Std.Do.PostCond α ps) => Q.fst a, conjunctive := ⋯ }
Instances For
Equations
- Std.Do.PredTrans.const p = { apply := fun (Q : Std.Do.PostCond α ps) => p, conjunctive := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Std.Do.PredTrans.instMonadLiftArg = { monadLift := fun {α : Type} (x : Std.Do.PredTrans m α) => Std.Do.PredTrans.pushArg (StateT.lift x) }
Equations
- Std.Do.PredTrans.instMonadLiftExcept = { monadLift := fun {α : Type} (x : Std.Do.PredTrans m α) => Std.Do.PredTrans.pushExcept (ExceptT.lift x) }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯