Weakest Preconditions and Dijkstra Monads

Prerequisites. Direct starred prerequisites: Chapter 42. No later core chapter depends on this route.

The type $F\mathsf{Nat}$ says that a computation may perform effects and return a natural number. It does not distinguish a state computation that increments its cell from one that resets the cell, nor an exception that is impossible from one that is inevitable. A specification must relate the initial state, the returned value, and every terminal outcome. An effect name does not contain that relation.

Postconditions determine preconditions

For a result type $A$, a postcondition is a predicate $p:A\to \mathsf{U}$. A total pure computation returning $a:A$ satisfies $p$ exactly when $p(a)$ holds. This forces the first predicate transformer.

For pure return and sequencing, the types force The calculation for two returns is The two tags name the displayed equations, not rules; the typing rules that carry the same names are introduced in definition 104.5. A postcondition alone is not a precondition until a computation determines how the two are connected.

For $\mathsf{incr}=\mathsf{get}()\mathsf{to}x\mathsf{in}\mathsf{put}(x+1)$, the state calculation is The first step uses two clauses at once: ${\mathsf{bind}}_{\mathsf{St}}$ hands ${\mathsf{get}}^{\mathsf{wp}}$ the continuation $\lambda (a,s_1).{\mathsf{put}}^{\mathsf{wp}}(a+1)(p)(s_1)$, and ${\mathsf{get}}^{\mathsf{wp}}$ applies it to $(s_0,s_0)$. Thus the desired contract is discharged by the arithmetic obligation .

Dijkstra monads from monads

Writing predicate transformers by hand risks choosing a return and bind that do not satisfy the monad equations. The source calculus $\mathsf{DM}$ instead starts with a computational monad and derives its specification by a selective continuation translation.

For the state monad $\mathsf{St}(A)=S\to \tau (A\times S)$, the translated type is $$\mathsf{St}(A{)}^{\star }=S\to ((A\times S)\to \mathsf{U})\to \mathsf{U},$$ which is ${\mathsf{WP}}_{\mathsf{St}}(A)$ up to argument order. Translating the monadic state return and bind gives exactly the clauses of definition 104.2.

Proof of Theorem 104.4 — CPS produces a Dijkstra monad

Proof. All three claims are proved by induction on the displayed $\mathsf{DM}$ typing derivation. We give the two monadic cases first, since every other case is homomorphic.

For return, the induction hypothesis gives ${\mathrm{\Delta }}^{\star }\mid {\mathrm{\Gamma }}^{\star }⊢e^{\star }:A^{\star }$. Hence $\lambda p.p(e^{\star }):(A^{\star }\to \mathsf{U})\to \mathsf{U}$. If $p\Rightarrow q$, application gives $p(e^{\star })\Rightarrow q(e^{\star })$. For a family $(p_i{)}_{i\in I}$, beta reduction gives $$({\mathsf{return}}_{\tau }e{)}^{\star }(\lambda a.\mathrm{\forall }i\in I.p_i(a))\equiv \mathrm{\forall }i\in I.p_i(e^{\star }),$$ which is the required conjunction.

For bind, inversion gives $e_1:A!\tau$ and $e_2:A^{\prime }!\tau$ under $x:A$. By the induction hypotheses, $e_1^{\star }$ and every substituted $e_2^{\star }[a/x]$ have the indicated predicate-transformer types. Thus $$\lambda p.e_1^{\star }(\lambda a.e_2^{\star }[a/x](p)):(A^{\prime \star }\to \mathsf{U})\to \mathsf{U}.$$ Given $p\Rightarrow q$, monotonicity of each $e_2^{\star }[a/x]$ gives $e_2^{\star }[a/x](p)\Rightarrow e_2^{\star }[a/x](q)$; monotonicity of $e_1^{\star }$ transports that pointwise implication. For conjunctions, conjunctivity of $e_2^{\star }[a/x]$ rewrites the continuation pointwise, and conjunctivity of $e_1^{\star }$ then distributes the outer transformer. This proves typing, monotonicity, and conjunctivity in the bind case.

For a variable or constant, the translated term has its translated declared type. Abstraction extends ${\mathrm{\Gamma }}^{\star }$ by the translated domain and uses the induction hypothesis on the body; application eliminates that arrow. Pairing, projections, injections, and case analysis apply their ordinary typing rules to the induction hypotheses. Their translated predicate transformers use postconditions only through translated subterms, so the preceding pointwise monotonicity and conjunction arguments apply component by component. These constructors and the two monadic forms exhaust the grammar in definition 104.3, completing claims 1 and 2.

For claim 3, induct on an equational derivation. Congruence cases follow from the induction hypotheses and congruence of the target theory. The beta, projection, and case equations translate to the corresponding target equations because the translation is homomorphic on those constructors. The return and bind equations translate by beta reduction. In particular, for all $w,k,h$ and postconditions $p$, The first two equations are beta reduction. Expanding both sides of the third gives $w(\lambda a.k(a)(\lambda b.h(b)(p)))$ on each side. Function extensionality in the target converts these pointwise equations into the three monad laws for $T^{\star }$. No constructor outside the displayed grammar occurs in the induction. ◻

For example, target left identity is the annotated calculation Monotonicity is not decoration, and one transformer at result type $A=\mathsf{Nat}$ shows what it excludes. Take $$w_{\mathrm{\neg }}(p):=(p(0)\to \mathrm{\perp }).$$ It is antitone: from $p\Rightarrow q$ one gets $w_{\mathrm{\neg }}(q)\Rightarrow w_{\mathrm{\neg }}(p)$, the implication running the wrong way. To exhibit the failure, choose two postconditions with $p\Rightarrow q$ and evaluate both at $0$: $$p(a):=\mathrm{\perp },q(a):=\mathbf{1}.$$ Then $p\Rightarrow q$ holds, $p(0)$ is false, and $q(0)$ is true. Hence $$w_{\mathrm{\neg }}(p)=(\mathrm{\perp }\to \mathrm{\perp })\text{is inhabited},w_{\mathrm{\neg }}(q)=(\mathbf{1}\to \mathrm{\perp })\text{is not},$$ so $w_{\mathrm{\neg }}(p)\Rightarrow w_{\mathrm{\neg }}(q)$ fails and $w_{\mathrm{\neg }}$ is not monotone. Weakening a postcondition should never strengthen the precondition it demands, and here it does. Clause 2 of theorem 104.4 is exactly what keeps $w_{\mathrm{\neg }}$ out of the generated interface: no source computation translates to it.

Computation types and verification conditions

Apply WP-Sub to $\mathsf{incr}$. Its inferred transformer is $$w_i(p)(s_0)=p(\mathsf{unit},s_0+1).$$ For the advertised transformer the verification condition is $$\mathrm{\forall }p,s_0.w_a(p)(s_0)\Rightarrow p(\mathsf{unit},s_0+1),$$ proved by instantiating $s_1=s_0+1$ and arithmetic. The solver may discharge that final formula, but the translation and soundness theorem determine why it is the right formula.

Proof of Theorem 104.7 — Conditional WP soundness for total computations

Proof. Suppose an infinite source reduction began at $e$. Strict forward simulation would concatenate its nonempty target segments into an infinite CIC reduction, contradicting clause 1. Hence $e$ has a normal form $n$. Clause 2 gives $\cdot ⊢n:\mathsf{Pure}Aw$. By clause 3, choose $v:A$ such that $$n=\mathsf{Pure}\mathsf{.}\mathsf{return}v,\mathrm{\forall }q:A\to \mathsf{U}.w(q)\Rightarrow q(v).$$ Specialize the second formula to $p$ and use the premise $w(p)$; this gives $p(v)$. The source rule R-Run removes the normal-form return, so $\mathsf{run}e{⟶}^{\ast }v$.

For the state clause, the displayed state representation and reification rule give $$(\mathsf{reify}e)s_0:\mathsf{Pure}(A\times S)(\lambda p.w(p)(s_0)).$$ Apply the pure clause with postcondition $p:(A\times S)\to \mathsf{U}$ and premise $w(p)(s_0)$. The resulting value is a pair $(v,s_1):A\times S$, and $p(v,s_1)$ holds. ◻

The passage from a closed normal form to a returned value uses clause 3 above. Consequently, the theorem records forward simulation and the canonical-return property as hypotheses rather than deriving them from the transformer laws.

Removing totality invalidates the step from normalization to a returned value. Removing monotonicity invalidates sequencing under a stronger postcondition. Removing the well-formed signature condition permits a claimed action whose implementation and transformer disagree. The theorem does not cover arbitrary handlers, general recursion, concurrency, or an external solver’s soundness.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 104.3, then complete exercise 104.5.

Exercise 104.3¶

★★☆ Prove right identity and associativity for ${\mathsf{bind}}_{\mathsf{St}}^{\mathsf{wp}}$ by annotated extensional calculations. Introduce every state and postcondition before use.

Referenced from 4 locations

• Weakest Preconditions and Dijkstra Monads
• ch:dijkstra-monads: Dijkstra monads

Exercise 104.4¶

★★★ Define two state-with-exception semantics, one preserving the state on failure and one rolling it back. Calculate one program on both. Show that their transformers disagree on a postcondition that inspects the exceptional state, so no theorem transfers without a rule delta.

Referenced from 3 locations

• Weakest Preconditions and Dijkstra Monads
• ch:dijkstra-monads: Dijkstra monads

Exercise 104.5¶

★★★ Practical project.dijkstra-vc-generator Implement in Kappa a predicate-transformer interpreter for return, bind, get, put, raise, and catch over finite integer states. Maintain monotonicity by constructing transformers only from the displayed clauses. The named acceptance cases are Require also the exact lines $$\begin{array}{c}\mathtt{\text{bind threads updated state}},\\ \mathtt{\text{catch handles the raised computation}},\\ \mathtt{\text{put changes the state seen by get}}.\end{array}$$ A mutation that resumes the bind body in the original state must fail increment vc valid and the first and third lines above while the checker itself remains well typed. Explain which occurrence of the intermediate state in ${\mathsf{bind}}_{\mathsf{St}}^{\mathsf{wp}}$ each failure exercises. The program decides finite verification conditions; it does not prove theorem 104.7 or justify an SMT solver.

Referenced from 5 locations

• Weakest Preconditions and Dijkstra Monads
• Erasure, dependent protocols, effects, specifications, and partiality: executable records
• ch:dijkstra-monads: finite verification conditions