def
Std.WP.Gadget.assertGadget
{m : Type u → Type v}
{Pred EPred : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
(as : Pred)
:
m PUnit
A no-op computation used as a verification gadget to inject assertions into the program.
The as parameter is the assertion to be checked. At runtime, assertGadget is simply
pure ⟨⟩.
Equations
Instances For
theorem
Std.WP.Spec.assertGadget
{m : Type u → Type v}
{Pred EPred : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{post : PUnit → Pred}
{epost : EPred}
(as : Pred)
[Lean.Order.Heyting Pred]
:
⦃ Lean.Order.meet as (Lean.Order.himp as (post PUnit.unit)) ⦄ Gadget.assertGadget as ⦃ post; epost ⦄
Specification for assertGadget: the precondition requires both the assertion as and
the Heyting implication as ⇨ post ⟨⟩, ensuring the assertion holds and the postcondition
follows from it.