Completeness

\(\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}} \)

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\),

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?

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} \]