Soundness
What questions do you have? What questions does your neighbor have?
Questions
Exercise: State Soundness and Completeness
State soundness and completeness of our program logic.
Exercise: Prove Soundness
Theorem 1 (Forwards Over-Approximation) If \(\mathcal{E} :: \rho \vdash s \Downarrow\rho'\) and \(\mathcal{V} :: {} \vdash \{\varphi\}\;s\;\{\varphi'\}\) such that \(\rho \models \varphi\), then \(\rho' \models \varphi'\).
Corollary 1 (Soundness of the Program Logic) If \( {} \vdash \{\varphi\}\;s\;\{\varphi'\}\), then \( \models \{\varphi\}\;s\;\{\varphi'\} \).
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 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?