Completeness
Tuesday, September 23, 2025
Meeting 10 - Completeness
What questions do you have? What questions does your neighbor have?
Questions
Review: Soundness
Prove Soundness
If \(\mathcal{E} :: \rho \vdash s \Downarrow\rho'\) and \(\mathcal{V} :: {} \vdash \{\varphi\}\;s\;\{\varphi'\}\) such that \(\rho \models \varphi\), then \(\rho' \models \varphi'\).
Proof. By nested induction on derivations \(\mathcal{E}\) and \(\mathcal{V}\). That is, we consider the well-founded lexicographic ordering on pairs \((\mathcal{E}, \mathcal{V})\).
- Case
- \(\mathcal{E} = \inferright{EvalSkip}{ }{ \rho \vdash \texttt{;} \Downarrow\rho }\) and \(\mathcal{V} = \inferright{VerifySkip}{ \phantom{\jhoare{}{}} }{ {} \vdash \{\varphi\}\; \texttt{;}\;\{\varphi\} }\)
| \(\rho' = \rho\) and \(\varphi' = \varphi\) | by assumption |
| \(\rho' \models \varphi'\) | by rewriting |
- Case
- \(\mathcal{E} = \inferright{EvalAssign}{ \mathcal{D}:: \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }\) and \(\mathcal{V} = \inferright{VerifyAssign}{ \phantom{\jhoare{}{}} }{ {} \vdash \{ [e/x]\varphi' \}\; x \mathrel{\texttt{=}}e \;\{ \varphi' \} }\)
| \(\rho \models [e/x]\varphi'\) | by assumption |
| \( \rho(x \leftarrow v) \models \varphi'\) | by Lemma 1 on \(\mathcal{D}\) |
- Case
- \(\mathcal{E} = \inferright{EvalSeq}{ \mathcal{E}_1 :: \rho \vdash s_1 \Downarrow\rho'' \and \mathcal{E}_2 :: \rho'' \vdash s_2 \Downarrow\rho' }{ \rho \vdash s_1 \mathbin{\texttt{;}} s_2 \Downarrow \rho' }\) and \(\mathcal{V} = \inferright{VerifySeq}{ \mathcal{V}_1 :: {} \vdash \{\varphi\}\; s_1 \;\{ \varphi'' \} \and \mathcal{V}_2 :: {} \vdash \{\varphi''\}\; s_2 \;\{ \varphi' \} }{ {} \vdash \{\varphi\}\; s_1 \mathbin{\texttt{;}} s_2 \;\{ \varphi' \} }\)
| \(\rho'' \models \varphi''\) | by the i.h. on \(\mathcal{E}_1\) and \(\mathcal{V}_1\) |
| \(\rho' \models \varphi'\) | by the i.h. on \(\mathcal{E}_2\) and \(\mathcal{V}_2\) |
- Case
- \(\mathcal{E} = \inferright{EvalIfTrue}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E}_1 :: \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\) and \(\mathcal{V} = \inferright{VerifyIf}{ \mathcal{V}_1 :: {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi'\} \and {} \vdash \{ \varphi \wedge\neg e \}\;s_2\;\{\varphi'\} }{ {} \vdash \{\varphi\}\; \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \;\{ \varphi' \} }\)
| \(\rho \models e\) | by definition of \( \models \) with \(\mathcal{D}\) |
| \(\rho \models \varphi \wedge e \) | by definition of \( \models \) |
| \(\rho' \models \varphi'\) | by the i.h. on \(\mathcal{E}_1\) and \(\mathcal{V}_1\) |
- Case
- \(\mathcal{E} = \inferright{EvalIfFalse}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{false} \and \mathcal{E}_2 :: \rho \vdash s_2 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\) and \(\mathcal{V} = \inferright{VerifyIf}{ {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi'\} \and \mathcal{V}_2 :: {} \vdash \{ \varphi \wedge\neg e \}\;s_2\;\{\varphi'\} }{ {} \vdash \{\varphi\}\; \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \;\{ \varphi' \} }\)
| \(\rho \models \neg e \) | by definition of \( \models \) with \(\mathcal{D}\) |
| \(\rho \models \varphi \wedge\neg e \) | by definition of \( \models \) |
| \(\rho' \models \varphi'\) | by the i.h. on \(\mathcal{E}_2\) and \(\mathcal{V}_2\) |
- Case
- \(\mathcal{E} = \inferright{EvalWhileFalse}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }\) and \(\mathcal{V} = \inferright{VerifyWhile}{ {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi\} }{ {} \vdash \{\varphi\}\; \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\{ \varphi \wedge\neg e \} }\)
| \(\rho \models \neg e \) | by definition of \( \models \) with \(\mathcal{D}\) |
| \(\rho \models \varphi \wedge\neg e \) | by definition of \( \models \) |
- Case
- \(\mathcal{E} = \inferright{EvalWhileTrue}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{true} \and \inferright{EvalSeq}{ \mathcal{E}_1 :: \rho \vdash s_1 \Downarrow\rho'' \and \mathcal{E}_2 :: \rho'' \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow\rho' }{ \rho \vdash s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho' } }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho' }\) and \(\mathcal{V} = \inferright{VerifyWhile}{ \mathcal{V}_1 :: {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi\} }{ {} \vdash \{\varphi\}\; \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\{ \varphi \wedge\neg e \} }\)
| \(\rho \models e\) | by definition of \( \models \) with \(\mathcal{D}\) |
| \(\rho \models \varphi \wedge e \) | by definition of \( \models \) |
| \(\rho'' \models \varphi\) | by the i.h. on \(\mathcal{E}_1\) and \(\mathcal{V}_1\) |
| \(\rho' \models \varphi \wedge\neg e \) | by the i.h. on \(\mathcal{E}_2\) and \(\mathcal{V}\) (N.B. on \(\mathcal{V}\)) |
- Case
- \(\mathcal{V} = \inferright{VerifyConsequence}{ \mathcal{D}_{\mathrm{pre}} :: \varphi_{\mathrm{pre}} \vdash \varphi_{\mathrm{pre}}' \and \mathcal{V}_1 :: {} \vdash \{\varphi_{\mathrm{pre}}'\}\; s\;\{\varphi_{\mathrm{post}}'\} \and \mathcal{D}_{\mathrm{post}} :: \varphi_{\mathrm{post}}' \vdash \varphi_{\mathrm{post}} }{ {} \vdash \{\varphi_{\mathrm{pre}}\}\; s\;\{\varphi_{\mathrm{post}}\} }\)
| \(\rho \models \varphi_{\mathrm{pre}}'\) | by Proposition 2 on \(\mathcal{D}_{\mathrm{pre}}\) |
| \(\rho' \models \varphi_{\mathrm{post}}'\) | by the i.h. on \(\mathcal{E}\) and \(\mathcal{V}_1\) (N.B. on \(\mathcal{E}\)) |
| \(\rho' \models \varphi_{\mathrm{post}}\) | by Proposition 2 on \(\mathcal{D}_{\mathrm{post}}\) |
Other cases for the pair of \(\mathcal{E}\) and \(\mathcal{V}\) are vacuously true, as the statement \(s\) would be different and hence contradictory.
Lemma: Substitution
Lemma 1 (Substitution on Store Assertions) If \(\rho \models [e/x]\varphi\) and \(\rho \vdash e \Downarrow v\), then \( \rho(x \leftarrow v) \models \varphi\).
Proof. By structural induction on \(\varphi\).
- Case
- \(\varphi= e_0\)
| \(\rho \vdash [e/x]e_0 \Downarrow \mathbf{true}\) | by definition of \( \models \) |
| \( \rho(x \leftarrow v) \vdash e_0 \Downarrow \mathbf{true}\) | by Proposition 1 |
| \( \rho(x \leftarrow v) \models \varphi\) | by definition of \( \models \) |
Other cases are as expected.
Proposition 1 (Substitution and Stores) If \(\rho \vdash [e/x]e_0 \Downarrow v_0\) and \(\rho \vdash e \Downarrow v\), then \( \rho(x \leftarrow v) \vdash e_0 \Downarrow v_0\).
Assumption: Soundness of the Assertion Logic
We define \(\Gamma \models \varphi\) iff
\(\rho \models \varphi_i\) for all \(\varphi_i \in \Gamma\) implies \(\rho \models \varphi\)
Proposition 2 (Soundness of the Assertion Logic) If \(\Gamma \vdash \varphi\), then \(\Gamma \models \varphi\).
Completeness
Completeness of the Program Logic
Proposition 3 (Completeness of the Program Logic) If \( \models \{\varphi\}\;s\;\{\varphi'\} \), then \( {} \vdash \{\varphi\}\;s\;\{\varphi'\}\).
Proposition 4 (Completeness of the Assertion Logic) If \(\Gamma \models \varphi\), then \(\Gamma \vdash \varphi\).
Unfortunately, for any interesting assertion logic, it must be incomplete and thus any program logic dependent on an interesting assertion logic is necessarily incomplete.
Proposition 5 (Relative Completeness of the Program Logic) If \( \models \{\varphi\}\;s\;\{\varphi'\} \) and the assertion logic \(\varphi\) is complete, then \( {} \vdash \{\varphi\}\;s\;\{\varphi'\}\).
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 6 (A Weakest Pre-Condition Exists) For all statements \(s\) and assertions \(\varphi\),
- (Weakest) \( \models \{\varphi_{\mathrm{pre}}\}\;s\;\{\varphi\} \) implies \(\varphi_{\mathrm{pre}} \models \operatorname{wp}(s, \varphi)\), and
- (Provable) the judgment \( {} \vdash \{ \operatorname{wp}(s, \varphi) \}\; s\;\{ \varphi\}\) holds.
Now what?
Relative Completeness
If \( \models \{\varphi\}\;s\;\{\varphi'\} \) and the assertion logic is complete (Proposition 4), then \(\mathcal{V} :: {} \vdash \{\varphi\}\;s\;\{\varphi'\}\).
Proof. Direct.
| \(\varphi \models \operatorname{wp}(s, \varphi') \) | by Proposition 6 (wp is weakest) |
| \(\mathcal{V}_1 :: {} \vdash \{ \operatorname{wp}(s, \varphi') \}\; s\;\{ \varphi' \}\) | by Proposition 6 (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 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} \]