Hoare Logic
What questions do you have? What questions does your neighbor have?
Exercise: JavaScripty Store Assertions
\[ \begin{array}{rrrl} \text{store assertions (i.e., symbolic stores)} & \varphi& \mathrel{::=}& e \\ && \mid& \top \mid\varphi_1 \wedge\varphi_2 \mid\bot \mid\varphi_1 \vee\varphi_2 \\ && \mid& \varphi_1 \Rightarrow\varphi_2 \mid\neg\varphi_1 \\ && \mid& \forall x.\varphi_1 \mid\exists x.\varphi_1 \\ \text{expressions} & e \\ \text{variables} & x \end{array} \]
Define the semantics of state assertions as a relation \(\rho \models \varphi\) by induction on the structure of the syntax of \(\varphi\). We read \(\rho \models \varphi\) as, “Store \(\rho\) satisfies (or, models) assertion \(\varphi\).” You may define this relation in terms of expression evaluation \(\rho \vdash e \Downarrow v\).
Exercise: JavaScripty Statement Assertions
Define the partial-correctness semantics of JavaScripty statements \( \models \{\varphi\}\;s\;\{\varphi'\} \).
Define the total-correctness semantics of JavaScripty statements \( \models [\varphi]\;s\;[\varphi'] \).
Preliminaries: Proof Systems
\[ \begin{array}{rrrl} \text{hypotheses} & \Gamma& \mathrel{::=}& \circ \mid\Gamma,\varphi \end{array} \]
We write \(\Gamma \vdash \varphi\) for the judgment that says, “Under hypotheses \(\Gamma\), store assertion \(\varphi\) is provable.”
We say that \(\Gamma \vdash \varphi\) is sound iff …
Exercise: A Program Logic for JavaScripty
Define a proof system for partial-correctness of JavaScripty statements, that is, a judgment form \( \vdash \{\varphi\}\;s\;\{\varphi'\} \) that says, “For all pre-stores that satisfy the pre-condition \(\varphi\), if \(s\) evaluates to a post-store, then the post-store satisfies the post-condition \(\varphi'\).”
Such a judgment form \( \vdash \{\varphi\}\;s\;\{\varphi'\} \) is called a program logic and defines an axiomatic semantics for JavaScripty statements \(s\).
Exercise: Program Verification
Prove using your program logic the following property: for any expression \(e\), if we evaluate the statement \[ s_{\text{even}}\colon\quad \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \]
in a pre-store in which \(\texttt{i}\) is even, and if \(s_{\text{even}}\) evaluates to a post-store, then \(\texttt{i}\) in that post-store is even.
Let us write \(\texttt{even}\texttt{(}x\texttt{)}\) for the expression that evaluates to \(\mathbf{true}\) when \(x\) is even.
Exercise: State Soundness and Completeness
State soundness and completeness of our program logic.
Exercise: Prove Soundness
Weakest Preconditions and 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 \( \models \{\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}}\).