Deductive Verification

Bor-Yuh Evan Chang

Tuesday, September 16, 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 8 - Deductive Verification

What questions do you have? What questions does your neighbor have?

Questions

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$.

JavaScripty Statements: Syntax

\[ \begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \texttt{;} \mid x \mathrel{\texttt{=}}e \mid s_1 \mathbin{\texttt{;}} s_2 \mid\mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \mid\mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \end{array} \]

Figure 1: Syntax of JavaScripty statements with assignment, sequencing, branching, and looping.

JavaScripty Statements: Big-Step Operational Semantics

\[ \fbox{$\rho \vdash s \Downarrow\rho'$} \]

$\inferrule[EvalSkip]{ \phantom{\Downarrow} }{ \rho \vdash \texttt{;} \Downarrow\rho }$

$\inferrule[EvalAssign]{ \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }$

$\inferrule[EvalSeq]{ \rho \vdash s_1 \Downarrow\rho' \and \rho' \vdash s_2 \Downarrow\rho'' }{ \rho \vdash s_1 \mathbin{\texttt{;}} s_2 \Downarrow \rho'' }$

$\inferrule[EvalIfTrue]{ \rho \vdash e \Downarrow\mathbf{true} \and \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }$

$\inferrule[EvalIfFalse]{ \rho \vdash e \Downarrow\mathbf{false} \and \rho \vdash s_2 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }$

$\inferrule[EvalWhileFalse]{ \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }$

$\inferrule[EvalWhileTrue]{ \rho \vdash e \Downarrow\mathbf{true} \and \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' }$

Figure 2: A big-step operational semantics for JavaScripty statements.

JavaScripty Statements: Axiomatic Semantics

\[ \fbox{$ {} \vdash \{\varphi\}\;s\;\{\varphi'\}$} \]

$\inferrule[VerifySkip]{ \phantom{\jhoare{}{}} }{ {} \vdash \{\varphi\}\; \texttt{;}\;\{\varphi\} }$

$\inferrule[VerifySeq]{ {} \vdash \{\varphi\}\; s_1 \;\{ \varphi' \} \and {} \vdash \{\varphi'\}\; s_2 \;\{ \varphi'' \} }{ {} \vdash \{\varphi\}\; s_1 \mathbin{\texttt{;}} s_2 \;\{ \varphi'' \} }$

$\inferrule[VerifyIf]{ {} \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' \} }$

$\inferrule[VerifyWhile]{ {} \vdash \{ \varphi \wedge e \}\;s_1\;\{\varphi\} }{ {} \vdash \{\varphi\}\; \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\{ \varphi \wedge\neg e \} }$

Figure 3: An axiomatic operational semantics for JavaScripty statements.

Assignment: Axiomatic Semantics

\[ \inferrule[VerifyAssign]{ \phantom{\jhoare{}{}} }{ {} \vdash \{\varphi\}\; x \mathrel{\texttt{=}}e \;\{ \exists x_{\mathrm{old}}. [x_{\mathrm{old}}/x]\varphi \wedge x= [x_{\mathrm{old}}/x]e \} } \]

Figure 4: A forwards assignment rule.

Assignment: Axiomatic Semantics

\[ \inferrule[VerifyAssign]{ \phantom{\jhoare{}{}} }{ {} \vdash \{ [e/x]\varphi \}\; x \mathrel{\texttt{=}}e \;\{ \varphi\} } \]

Figure 5: A backwards assignment rule.

Capture-Avoiding Substitution

We write $[e/x]\varphi$ for the capture-avoiding substitution of expression $e$ for free-uses of variable $x$ in symbolic store $\varphi$. Capture-avoiding means that bound-variables in the symbolic store $\varphi$ are renamed consistently so that they do not clash with free variables in replacement expression $e$ before textual substituation. Renaming of bound-variables consistently is called $\alpha$-renaming.

Rule of Consequence

\[ \inferrule[VerifyConsequence]{ \varphi_{\mathrm{pre}} \vdash \varphi_{\mathrm{pre}}' \and {} \vdash \{\varphi_{\mathrm{pre}}'\}\; s\;\{\varphi_{\mathrm{post}}'\} \and \varphi_{\mathrm{post}}' \vdash \varphi_{\mathrm{post}} }{ {} \vdash \{\varphi_{\mathrm{pre}}\}\; s\;\{\varphi_{\mathrm{post}}\} } \]

Figure 6: The rule of consequence.

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.

Program Verification

Theorem 1 (Evenness Invariant, Axiomatically) Let us write $\texttt{even}\texttt{(}x\texttt{)}$ for the expression that evaluates to $\mathbf{true}$ when $x$ is even. For any expression $e$, we have that \[ \mathcal{V} :: {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \}\; \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} \]

Proof. Direct.

$\mathcal{V}_1 = \inferright{VerifyAssign}{ }{ {} \vdash \{ \texttt{even}\texttt{(} \texttt{i}+ 2 \texttt{)} \}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} }$	by definition
$\mathcal{P}_1 :: \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge e \vdash \texttt{even}\texttt{(}\texttt{i}+ 2\texttt{)} $	by logic and arithmetic
$\mathcal{P}_2 :: \texttt{even}\texttt{(}\texttt{i}\texttt{)} \vdash \texttt{even}\texttt{(}\texttt{i}\texttt{)} $	by logic
$\mathcal{V}_2 = \inferright{VerifyConsequence}{ \mathcal{P}_1 \and \mathcal{V}_1 \and \mathcal{P}_2 }{ {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge e \}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} }$	by definition
$\mathcal{V}_3 = \inferright{VerifyWhile}{ \mathcal{V_2} }{ {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \}\; \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge\neg e \} }$	by definition
$\mathcal{P}_3 :: \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge\neg e \vdash \texttt{even}\texttt{(}\texttt{i}\texttt{)} $	by logic
$\mathcal{V} = \inferright{VerifyConsequence}{ \mathcal{P}_2 \and \mathcal{V}_3 \and \mathcal{P}_3 }{ {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \}\; \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} }$	by definition

Program Verification

We can abbreviate the above derivation $\mathcal{V}$ by annotating the program with assertions:

{ even(i) }
while (e) {
  { even(i + 2) && e }
  { even(i + 2) }
  i = i + 2
  { even(i) }
}
{ even(i) && !e }
{ even(i) }

The assertions immediately around a statement is an application of the $\TirName{Verify}$ rule for the statement form, while two adjacent assertions without an intermediate statement is an application of $\TirName{VerifyConsequence}$.

Exercise: State Soundness and Completeness

State soundness and completeness of our program logic.

Exercise: Prove Soundness

Theorem 2 (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'\} $.

\(\mathcal{V}_1 = \inferright{VerifyAssign}{ }{ {} \vdash \{ \texttt{even}\texttt{(} \texttt{i}+ 2 \texttt{)} \}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} }\)	by definition
\(\mathcal{P}_1 :: \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge e \vdash \texttt{even}\texttt{(}\texttt{i}+ 2\texttt{)} \)	by logic and arithmetic
\(\mathcal{P}_2 :: \texttt{even}\texttt{(}\texttt{i}\texttt{)} \vdash \texttt{even}\texttt{(}\texttt{i}\texttt{)} \)	by logic
\(\mathcal{V}_2 = \inferright{VerifyConsequence}{ \mathcal{P}_1 \and \mathcal{V}_1 \and \mathcal{P}_2 }{ {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge e \}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} }\)	by definition
\(\mathcal{V}_3 = \inferright{VerifyWhile}{ \mathcal{V_2} }{ {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \}\; \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge\neg e \} }\)	by definition
\(\mathcal{P}_3 :: \texttt{even}\texttt{(}\texttt{i}\texttt{)} \wedge\neg e \vdash \texttt{even}\texttt{(}\texttt{i}\texttt{)} \)	by logic
\(\mathcal{V} = \inferright{VerifyConsequence}{ \mathcal{P}_2 \and \mathcal{V}_3 \and \mathcal{P}_3 }{ {} \vdash \{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \}\; \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \;\{ \texttt{even}\texttt{(}\texttt{i}\texttt{)} \} }\)	by definition