def Std.WP.Gadget.assertGadget {m : Type u → Type v} {Pred EPosts : Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] (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 EPosts : Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {post : PUnit → Pred} {eposts : EPosts} (as : Pred) [Lean.Order.Heyting Pred] :
⦃ Lean.Order.meet as (Lean.Order.himp as (post PUnit.unit)) ⦄ Gadget.assertGadget as ⦃ post; eposts ⦄
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.