Documentation

Std.Do.WP.Basic

Weakest precondition interpretation #

This module defines the weakest precondition interpretation WP of monadic programs in terms of predicate transformers PredTrans.

This interpretation forms the basis of our notion of Hoare triples. It is the main mechanism of this library for reasoning about monadic programs.

An instance WP m ps determines an interpretation wp⟦x⟧ of a program x : m α in terms of a predicate transformer PredTrans ps α; The monad m determines ps : PostShape and hence the particular shape of the predicate transformer.

This library comes with pre-defined instances for common monads and transformers such as

These instances are all monad morphisms, a fact which is properly encoded and exploited by the subclass WPMonad.

class Std.Do.WP (m : TypeType u) (ps : outParam PostShape) :
Type (max 1 u)

A weakest precondition interpretation of a monadic program x : m α in terms of a predicate transformer PredTrans ps α. The monad m determines ps : PostShape. See the module comment for more details.

Instances
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        instance Std.Do.StateT.instWP {m : TypeType u} {ps : PostShape} {σ : Type} [WP m ps] :
        WP (StateT σ m) (PostShape.arg σ ps)
        Equations
        instance Std.Do.ReaderT.instWP {m : TypeType u} {ps : PostShape} {ρ : Type} [WP m ps] :
        WP (ReaderT ρ m) (PostShape.arg ρ ps)
        Equations
        instance Std.Do.ExceptT.instWP {m : TypeType u} {ps : PostShape} {ε : Type} [WP m ps] :
        WP (ExceptT ε m) (PostShape.except ε ps)
        Equations
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Std.Do.Id.by_wp {α : Type} {x : α} {prog : Id α} (h : prog.run = x) (P : αProp) :
        wp⟦prog (Std.Do.PostCond.total P)P x
        theorem Std.Do.StateM.by_wp {σ : Type} {s : σ} {α : Type} {x : α × σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σProp) :
        wp⟦prog (⇓ (a : α) (s' : σ) => P (a, s')) sP x
        theorem Std.Do.EStateM.by_wp {ε σ : Type} {s : σ} {α : Type} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} (h : prog.run s = x) (P : EStateM.Result ε σ αProp) :
        wp⟦prog (⇓ (a : α) (s' : σ) => P (EStateM.Result.ok a s')) sP x