Hoare Logic

Bor-Yuh Evan Chang

Thursday, September 11, 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 7 - 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} \]

Figure 1: Syntax of JavaScripty store assertions (first-order logic).

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