Weakest Precondition Interpretation

WP Prog Value Pred EPred interprets a program type Prog whose results have type Value as a monotone predicate transformer PredTrans Pred EPred Value. For a program x : Prog, a normal postcondition post : Value → Pred and an exception postcondition epost : EPred, the assertion wp x post epost is the weakest precondition under which x establishes post and epost.

The program type Prog determines the other three types, which are outParams of the class. Instance search runs on Prog alone. A term wp x post epost therefore fixes the result type, the assertion lattice and the exception postcondition type from the type of x, and each program type carries one interpretation.

Two examples show the range of Prog. The error-state monad EStateM ε σ has the instance WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop). Here a state predicate is the assertion, and an error paired with a state is the exception postcondition.

A deep embedding is the second example. A command language Cmd with assertions Env → State → Prop has the instance WP Cmd Unit (Env → State → Prop) EStack⟨⟩. Its wp is defined in terms of an operational semantics such as an omnisemantics. The file tests/elab/vcgenImp.lean carries this example in full.

Everything here is generic over the program type. The interpretation of a monad and of the monad transformers is in Std.WP.Monad.

Assertion Language Classes

Assertion is an alias type class for CompleteLattice. We use Assertion Pred for the assertion language of normal postconditions and Assertion EPred for exception postconditions.

The WP Typeclass

The WP typeclass interprets a program type Prog whose results have type Value as a monotone predicate transformer wpTrans : Prog → PredTrans Pred EPred Value.

class Std.WP.WP (Prog : Type u) (Value : outParam (Type v)) (Pred : outParam (Type w)) (EPred : outParam (Type w')) [Assertion Pred] [Assertion EPred] : Type (max (max (max u v) w) w')

Weakest precondition interpretation of a program type Prog whose results have type Value, as a monotone predicate transformer over assertion language Pred with exception postconditions EPred.

• wpTrans : Prog → Lean.Order.PredTrans Pred EPred Value

  The weakest precondition transformer for a program.

• wp_trans_monotone (x : Prog) : (wpTrans x).monotone

  Monotonicity: weaker postconditions yield weaker preconditions.

def Std.WP.WP.wp {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type w'} [Assertion Pred] [Assertion EPred] [self : WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost : EPred) : Pred

Weakest precondition of x for normal postcondition post and exception postcondition epost. The WP interpretation can be supplied explicitly via dot notation (inst.wp x post epost).

Equations

• Std.WP.wp x post epost = (Std.WP.WP.wpTrans x).apply post epost

@[simp]

theorem Std.WP.WP.wpTrans_apply_eq {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) : (wpTrans x).apply = wp x

Derived WP Lemmas

Monotonicity and weakening consequences of the WP monotonicity axiom.

theorem Std.WP.WP.wp_consequence {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post post' : Value → Pred) (epost : EPred) (h : Lean.Order.PartialOrder.rel post post') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post' epost)

theorem Std.WP.WP.wp_consequence_econs {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post post' : Value → Pred) (epost epost' : EPred) (h : Lean.Order.PartialOrder.rel post post') (h' : Lean.Order.PartialOrder.rel epost epost') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post' epost')

theorem Std.WP.WP.wp_econs {Pred : Type u_2} {EPred : Type u_1} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost epost' : EPred) (h' : Lean.Order.PartialOrder.rel epost epost') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post epost')

theorem Std.WP.WP.wp_econs_bot {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x post Lean.Order.bot) (wp x post epost)

theorem Std.WP.WP.wp_consequence_le {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post post' : Value → Pred) (epost : EPred) (h : Lean.Order.PartialOrder.rel post post') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post epost)) : Lean.Order.PartialOrder.rel pre (wp x post' epost)

theorem Std.WP.WP.wp_econs_le {Pred : Type u_2} {EPred : Type u_1} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost epost' : EPred) (h : Lean.Order.PartialOrder.rel epost epost') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post epost)) : Lean.Order.PartialOrder.rel pre (wp x post epost')

theorem Std.WP.WP.wp_econs_bot_le {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost : EPred) {pre : Pred} (h : Lean.Order.PartialOrder.rel pre (wp x post Lean.Order.bot)) : Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.WP.wp_le_wp_of_eq {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x y : Prog} (h : x = y) (post : Value → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp y post epost) (wp x post epost)

Rewriting the program of a weakest precondition along an equation x = y weakens it: the precondition of y entails the precondition of x.