Verification Conditions

Bor-Yuh Evan Chang

Thursday, September 25, 2025

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Meeting 11 - Verification Conditions

What questions do you have? What questions does your neighbor have?

Announcements

Questions?

Review: Weakest Preconditions and Relative Completeness

What if for a post-condition \(\varphi_{\mathrm{post}}\) and a statement \(s\), we could define the weakest pre-condition \(\varphi_{\mathrm{weakest}}\) such that \( {} \vdash \{\varphi_{\mathrm{weakest}}\}\;s\;\{\varphi_{\mathrm{post}}\}\)? That is, for all pre-conditions \(\varphi_{\mathrm{pre}}\) such that \( \models \{\varphi_{\mathrm{pre}}\}\;s\;\{\varphi_{\mathrm{post}}\} \), we have that \(\varphi_{\mathrm{pre}} \models \varphi_{\mathrm{weakest}}\) and \( {} \vdash \{\varphi_{\mathrm{weakest}}\}\;s\;\{\varphi_{\mathrm{post}}\}\).

We write \(\operatorname{wp}(s, \varphi_{\mathrm{post}})\) for this weakest pre-condition for a statement \(s\) and a post-condition \(\varphi_{\mathrm{post}}\).

Proposition 1 (A Weakest Pre-Condition Exists) For all statements \(s\) and assertions \(\varphi\),

1. (Weakest) \( \models \{\varphi_{\mathrm{pre}}\}\;s\;\{\varphi\} \) implies \(\varphi_{\mathrm{pre}} \models \operatorname{wp}(s, \varphi)\), and
2. (Provable) the judgment \( {} \vdash \{ \operatorname{wp}(s, \varphi) \}\; s\;\{ \varphi\}\) holds.

Now what?

Review: Relative Completeness

If \( \models \{\varphi\}\;s\;\{\varphi'\} \) and the assertion logic is complete, then \(\mathcal{V} :: {} \vdash \{\varphi\}\;s\;\{\varphi'\}\).

Proof. Direct.

\(\varphi \models \operatorname{wp}(s, \varphi') \)	by Proposition 1 (wp is weakest)
\(\mathcal{V}_1 :: {} \vdash \{ \operatorname{wp}(s, \varphi') \}\; s\;\{ \varphi' \}\)	by Proposition 1 (wp is provable)
\(\mathcal{P}_1 :: \varphi \vdash \operatorname{wp}(s, \varphi') \)	by the assumption that the assertion logic is complete
\(\mathcal{P}_2 :: \varphi' \vdash \varphi' \)	by logic
\(\mathcal{V} = \inferright{VerifyConsequence}{ \mathcal{P}_1 \and \mathcal{V}_1 \and \mathcal{P}_2 }{ {} \vdash \{\varphi\}\; s\;\{\varphi'\} }\)	by definition

Exercise: Weakest Pre-Condition

Define \(\operatorname{wp}(s, \varphi)\) by induction on the structure of \(s\), following the judgment form \( {} \vdash \{\varphi\}\;s\;\{\varphi'\}\)

Weakest Pre-Condition

\[ \begin{array}{rrl} \operatorname{wp}( \texttt{;}, \varphi) & \mathrel{:=}& \varphi \\ \operatorname{wp}( x \mathrel{\texttt{=}}e , \varphi) & \mathrel{:=}& [e/x]\varphi \\ \operatorname{wp}( \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 , \varphi) & \mathrel{:=}& (e \Rightarrow\operatorname{wp}(s_1, \varphi)) \wedge (\neg e \Rightarrow\operatorname{wp}(s_2, \varphi)) \\ \end{array} \]

Weakest Pre-Condition for While

\[ \begin{array}{rrl} \operatorname{wp}( \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 , \varphi) & \mathrel{:=}& (\neg e \Rightarrow \varphi) \wedge (e \Rightarrow \operatorname{wp}(s_1, \neg e \Rightarrow \varphi ) ) \wedge \cdots \end{array} \]

Weakest Pre-Condition for While

\[ \begin{array}{rrl} \operatorname{wp}( \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 , \varphi) & \mathrel{:=}& \bigwedge_i \operatorname{wp}_{i}^{\mathbf{while}\texttt{(}e\texttt{)}s_1}(\varphi) \\ \\ \operatorname{wp}_{0}^{\mathbf{while}\texttt{(}e\texttt{)}s}(\varphi) & \mathrel{:=}& \neg e \Rightarrow \varphi \\ \operatorname{wp}_{i + 1}^{\mathbf{while}\texttt{(}e\texttt{)}s}(\varphi) & \mathrel{:=}& e \Rightarrow \operatorname{wp}(s, \operatorname{wp}_{i}^{\mathbf{while}\texttt{(}e\texttt{)}s}(\varphi) ) \end{array} \]

Need to prove Proposition 1 for the above definition of \(\operatorname{wp}(e, s)\).

Weakest pre-conditions are impossible to compute (in general). Could we compute “almost weakest” pre-condition?

Verification Conditions

Predicate Transformers

We call a function like \(\operatorname{wp}\) a predicate transformer, as it transforms a store assertion with respect to the effect of a statement (e.g., a post-condition \(\varphi_{\mathrm{post}}\) into a pre-condition \(\varphi_{\mathrm{pre}}\) with respect to a statement \(s\)).

Verification Conditions

A verification condition is …

… a compilation of a program assertion into a store assertion (like \(\operatorname{wp}\) but computable) that over-approximates the effect of the program (e.g., generates assertions that may be weaker than the \(\operatorname{wp}\)).

A Verification-Condition Generator (VCGen)

\[ \begin{array}{rrl} \operatorname{vc}( \texttt{;}, \varphi_{\mathrm{post}}) & \mathrel{:=}& \varphi_{\mathrm{post}} \\ \operatorname{vc}( s_1 \mathbin{\texttt{;}} s_2 , \varphi_{\mathrm{post}}) & \mathrel{:=}& \operatorname{vc}(s_1, \operatorname{vc}(s_2, \varphi_{\mathrm{post}})) \\ \operatorname{vc}( x \mathrel{\texttt{=}}e , \varphi_{\mathrm{post}}) & \mathrel{:=}& [e/x]\varphi_{\mathrm{post}} \\ \operatorname{vc}( \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 , \varphi_{\mathrm{post}}) & \mathrel{:=}& (e \Rightarrow\operatorname{vc}(s_1, \varphi_{\mathrm{post}})) \wedge (\neg e \Rightarrow\operatorname{vc}(s_2, \varphi_{\mathrm{post}})) \end{array} \]

Exercise: A VCGen for While

\[ \begin{array}{rrl} \operatorname{vc}( \mathbf{while}_{\varphi_{\mathrm{inv}}}\;\texttt{(}e\texttt{)}\;s_1 , \varphi_{\mathrm{post}}) & \mathrel{:=}& ? \end{array} \]

Consider a verification condition for the example:

\[ \begin{array}{rrl} \operatorname{vc}( \mathbf{while}_{\texttt{even}\texttt{(}\texttt{i}\texttt{)}}\;\texttt{(}e\texttt{)}\;\texttt{i} \mathrel{\texttt{=}}\texttt{i} \mathbin{\texttt{+}} \texttt{2} , \texttt{even}\texttt{(}\texttt{i}\texttt{)}) & = & ? \end{array} \]

A VCGen for While

Let us write \(\operatorname{mod}(s)\) for the variables modified by statement \(s\).

\[ \begin{array}{l} \operatorname{vc}( \mathbf{while}_{\varphi_{\mathrm{inv}}}\;\texttt{(}e\texttt{)}\;s_1 , \varphi_{\mathrm{post}}) \quad \mathrel{:=} \\ \begin{array}{ll} \quad \varphi_{\mathrm{inv}}\;\wedge& \text{The loop invariant holds on entry.} \\ \quad\quad \forall \operatorname{mod}(s_1). & \text{Havoc the variables modified by the loop,} \\ \quad\quad\quad \varphi_{\mathrm{inv}}\Rightarrow& \text{except assuming the loop invariant.} \\ \quad\quad\quad\quad (e\Rightarrow\operatorname{vc}(s_1, \varphi_{\mathrm{inv}}) \;\wedge& \text{If the loop continues, the loop's effect preserves the invariant.} \\ \quad\quad\quad\quad \phantom{(}\neg e\Rightarrow\varphi_{\mathrm{post}}) & \text{Otherwise, if the loop exits, the post-condition is implied.} \\ \end{array} \end{array} \]

An Example VC

\[ \begin{array}{l} \operatorname{vc}( \mathbf{while}_{\texttt{even}\texttt{(}\texttt{i}\texttt{)}}\;\texttt{(}e\texttt{)}\;\texttt{i} \mathrel{\texttt{=}}\texttt{i} \mathbin{\texttt{+}} \texttt{2} , \texttt{even}\texttt{(}\texttt{i}\texttt{)}) \colon \\ \begin{array}{ll} \quad \texttt{even}\texttt{(}\texttt{i}\texttt{)}\;\wedge& \text{The loop invariant holds on entry.} \\ \quad\quad \forall \texttt{i}. & \text{Havoc the variables modified by the loop,} \\ \quad\quad\quad \texttt{even}\texttt{(}\texttt{i}\texttt{)}\Rightarrow& \text{except assuming the loop invariant.} \\ \quad\quad\quad\quad (e\Rightarrow\texttt{even}\texttt{(} \texttt{i} \mathbin{\texttt{+}} \texttt{2}\texttt{)} \;\wedge& \text{If the loop continues, the loop's effect preserves the invariant.} \\ \quad\quad\quad\quad \phantom{(}\neg e\Rightarrow\texttt{even}\texttt{(}\texttt{i}\texttt{)}) & \text{Otherwise, if the loop exits, the post-condition is implied.} \\ \end{array} \end{array} \]