Assertions
What questions do you have? What questions does your neighbor have?
Announcements
- Reminder: Reading/Post-Lecture Assignments
- Post \(\ge\) 1 substantive comment, question, or answer for each lecture
- Due before the next meeting
Questions?
Exercise: Meta Theory
Prove an equivalence between big-step evaluation and small-step reduction. You will first need to define iterating the small-step relation to state the theorem. Then, you will need to come up with a lemma that relates single-step reduction with evaluation.
Review: Reachabilty in a Transition System
Consider the reflexive-transitive closure of the small-step relation defined as follows:
\[ \fbox{$\langle \rho, s \rangle \rightarrow^{\ast}\langle \rho', s' \rangle$} \]
\(\inferrule[ReachRefl]{ \phantom{ \langle \rho, \rangle } }{ \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho, s \rangle }\)
\(\inferrule[ReachTrans]{ \langle \rho, s \rangle \rightarrow \langle \rho', s' \rangle \and \langle \rho', s' \rangle \rightarrow^{\ast} \langle \rho'', s'' \rangle }{ \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho'', s'' \rangle }\)
Review: Big-Step Implies Small-Step
Theorem 1 (Evaluation implies reduction) If \(\mathcal{E} :: \rho \vdash s \Downarrow\rho'\), then \(\mathcal{M} :: \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \)
Proof. By structural induction on derivation \(\mathcal{E}\).
- Case
- \(\mathcal{E} = \inferright{EvalSkip}{ }{ \rho \vdash \texttt{;} \Downarrow\rho }\)
| \(\mathcal{M} = \inferright{ReachRefl}{ }{ \langle \rho, \texttt{;} \rangle \rightarrow^{\ast} \langle \rho, \texttt{;} \rangle }\) | by definition |
- Case
- \(\mathcal{E} = \inferright{EvalAssign}{ \mathcal{E_1} :: \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }\)
| \(\rho' = \rho(x \leftarrow v)\) | by assumption |
| \(\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoAssign}{ \mathcal{E_1} :: \rho \vdash e \Downarrow v }{ \langle \rho, x \mathrel{\texttt{=}}e \rangle \rightarrow \langle \rho' , \texttt{;} \rangle } \and \inferright{ReachRefl}{ }{ \langle \rho', \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, x \mathrel{\texttt{=}}e \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
- 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' }\)
| \(\mathcal{M_1} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle \) | by the i.h. on \(\mathcal{E_1}\) |
| \(\mathcal{M_2} :: \langle \rho'', s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \) | by the i.h. on \(\mathcal{E_2}\) |
| \(\mathcal{M} :: \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \) | by Lemma 1 on \(\mathcal{M_1}\) and \(\mathcal{M_2}\) |
- Case
- \(\mathcal{E} = \inferright{EvalIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E_2} :: \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\)
| \(\mathcal{E_{21}} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \) | by the i.h. on \(\mathcal{E_2}\) |
| \(\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_1 \rangle } \and \mathcal{E_{21}} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
- Case
- \(\mathcal{E} = \inferright{EvalIfFalse}{ \mathcal{E_1} :: \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' }\)
| \(\mathcal{E_{21}} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \) | by the i.h. on \(\mathcal{E_2}\) |
| \(\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoIfFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_2 \rangle } \and \mathcal{E_{21}} :: \langle \rho, s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
- Case
- \(\mathcal{E} = \inferright{EvalWhileFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }\)
| \(\mathcal{S_1} = \inferright{DoWhile}{ }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }\) | by definition |
| \(\mathcal{M} = \inferright{ReachTrans}{ \mathcal{S_1} \and \inferright{ReachTrans}{ \inferright{DoIfFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\;\texttt{;} \rangle \rightarrow \langle \rho, \texttt{;} \rangle } \and \inferright{ReachRefl}{ }{ \langle \rho', \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho', \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
- Case
- \(\mathcal{E} = \inferright{EvalWhileTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E_2} :: \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' }\)
| \(\mathcal{S_1} = \inferright{DoWhile}{ }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }\) | by definition |
| \(\mathcal{M_2} :: \langle \rho, s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \) | by the i.h. on \(\mathcal{E_2}\) |
| \(\mathcal{M} = \inferright{ReachTrans}{ \mathcal{S_1} \and \inferright{ReachTrans}{ \inferright{DoIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\;\texttt{;} \rangle \rightarrow \langle \rho, s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle } \and \mathcal{M_2} }{ \langle \rho', \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
Review: Lemma: Sequential Composition
Lemma 1 (Reduction composes sequentially) If \(\mathcal{M_1} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle \) and \(\mathcal{M_2} :: \langle \rho'', s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \), then \(\mathcal{M} :: \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \)
Proof. By structural induction on derivation \(\mathcal{M_1}\).
Lemma: Sequential Composition
Proof. By structural induction on derivation \(\mathcal{M_1}\).
- Case
- \(\mathcal{M_1} = \inferright{ReachRefl}{ }{ \langle \rho, \texttt{;} \rangle \rightarrow^{\ast} \langle \rho, \texttt{;} \rangle }\)
| \(\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoSeq}{ }{ \langle \rho, \texttt{;} \mathbin{\texttt{;}} s_2 \rangle \rightarrow \langle \rho, s_2 \rangle } \and \mathcal{M_2} :: \langle \rho, s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, \texttt{;} \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
- Case
- \(\mathcal{M_1} = \inferright{ReachTrans}{ \mathcal{S_{11}} :: \langle \rho, s_1 \rangle \rightarrow \langle \rho''', s_1' \rangle \and \mathcal{M_{12}} :: \langle \rho''', s_1' \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle }{ \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle }\)
| \(\mathcal{M'} :: \langle \rho''', s_1' \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \) | by the i.h. on \(\mathcal{M_{12}}\) with \(\mathcal{M_{2}}\) |
| \(\mathcal{M} = \inferright{ReachTrans}{ \inferright{SearchSeq}{ \mathcal{S_{11}} :: \langle \rho, s_1 \rangle \rightarrow \langle \rho''', s_1' \rangle }{ \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow \langle \rho''', s_1' \mathbin{\texttt{;}} s_2 \rangle } \and \mathcal{M'} :: \langle \rho''', s_1' \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\) | by definition |
Exercise: Small-Step Implies Big-Step
Theorem 2 (Reduction implies evaluation) If \(\mathcal{M} :: \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \), then \(\mathcal{E} :: \rho \vdash s \Downarrow\rho'\).
Proof. By structural induction on derivation \(\mathcal{M}\).
Small-Step Implies Big-Step
Proof. By structural induction on derivation \(\mathcal{M}\).
- Case
- \(\mathcal{M} = \inferright{ReachRefl}{ }{ \langle \rho, \texttt{;} \rangle \rightarrow^{\ast} \langle \rho, \texttt{;} \rangle }\)
| \(\mathcal{E} = \inferright{EvalSkip}{ }{ \rho \vdash \texttt{;} \Downarrow\rho }\) | by definition |
- Case
- \(\mathcal{M} = \inferright{ReachTrans}{ \mathcal{S_1} :: \langle \rho, s \rangle \rightarrow \langle \rho'', s' \rangle \and \mathcal{M_2} :: \langle \rho'', s' \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\)
| \(\mathcal{E_2} :: \rho'' \vdash s' \Downarrow\rho'\) | by the i.h. on \(\mathcal{M_2}\) |
| \(\mathcal{E} :: \rho \vdash s \Downarrow\rho'\) | by Lemma 2 on \(\mathcal{S_1}\) and \(\mathcal{E_2}\) |
Lemma: Closed under Head Expansion
Lemma 2 (Evaluation is closed under head expansion) If \(\mathcal{S} :: \langle \rho, s \rangle \rightarrow \langle \rho'', s' \rangle \) and \(\mathcal{E} :: \rho'' \vdash s' \Downarrow\rho'\), then \(\mathcal{E'} :: \rho \vdash s \Downarrow\rho'\).
Proof. By structural induction on derivation \(\mathcal{S}\).
Lemma: Closed under Head Expansion
Proof. By structural induction on derivation \(\mathcal{S}\).
- Case
- \(\mathcal{S} = \inferright{DoAssign}{ \mathcal{D}:: \rho \vdash e \Downarrow v }{ \langle \rho, x \mathrel{\texttt{=}}e \rangle \rightarrow \langle \rho(x \leftarrow v) , \texttt{;} \rangle }\)
| \(\rho'' = \rho(x \leftarrow v)\) | by assumption |
| \(\rho' = \rho''\) | by inversion on \(\mathcal{E}\) |
| \(\mathcal{E'} = \inferright{EvalAssign}{ \mathcal{D}:: \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }\) | by definition |
- Case
- \(\mathcal{S} = \inferright{DoSeq}{ }{ \langle \rho, \texttt{;} \mathbin{\texttt{;}} s_1 \rangle \rightarrow \langle \rho, s_1 \rangle }\)
| \(\rho'' = \rho\) and \(s' = s_1\) | by assumption |
| \(\mathcal{E'} = \inferright{EvalSeq}{ \inferright{EvalSkip}{ }{ \rho \vdash \texttt{;} \Downarrow\rho } \and \mathcal{E} :: \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \texttt{;} \mathbin{\texttt{;}} s_1 \Downarrow\rho' }\) | by definition |
- Case
- \(\mathcal{S} = \inferright{DoIfTrue}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_1 \rangle }\)
| \(\rho'' = \rho\) and \(s' = s_1\) | by assumption |
| \(\mathcal{E'} = \inferright{EvalIfTrue}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E} :: \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow\rho' }\) | by definition |
- Case
- \(\mathcal{S} = \inferright{DoIfFalse}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{false} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_2 \rangle }\)
| \(\rho'' = \rho\) and \(s' = s_2\) | by assumption |
| \(\mathcal{E'} = \inferright{EvalIfFalse}{ \mathcal{D}:: \rho \vdash e \Downarrow\mathbf{false} \and \mathcal{E} :: \rho \vdash s_2 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow\rho' }\) | by definition |
- Case
- \(\mathcal{S} = \inferright{DoWhile}{ }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }\)
| \(\rho'' = \rho\) and \(s' = \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\;\texttt{;}\) | by assumption |
| \(\mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true}\) and \(\mathcal{E_2} :: \rho \vdash s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow\rho'\); or \(\mathcal{E_1'} :: \rho \vdash e \Downarrow\mathbf{false}\) and \(\mathcal{E_2'} :: \rho \vdash \texttt{;} \Downarrow\rho'\) | by inversion on \(\mathcal{E}\) |
- Subcase
- \(\mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true}\) and \(\mathcal{E_2}\)
| \(\mathcal{E'} = \inferright{EvalWhileTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E_2} :: \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' }\) | by definition |
- Subcase
- \(\mathcal{E_1'} :: \rho \vdash e \Downarrow\mathbf{false}\) and \(\mathcal{E_2'}\)
| \(\mathcal{E'} = \inferright{EvalWhileTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }\) | by definition |
| \(\rho' = \rho\) | by inversion on \(\mathcal{E_2'}\) |
- Case
- \(\mathcal{S} = \inferright{SearchSeq}{ \mathcal{S_1} :: \langle \rho, s_1 \rangle \rightarrow \langle \rho'', s_1' \rangle }{ \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow \langle \rho'', s_1' \mathbin{\texttt{;}} s_2 \rangle }\)
| \(\mathcal{E_1} :: \rho'' \vdash s_1' \Downarrow\rho'''\) and \(\mathcal{E_2} :: \rho''' \vdash s_2 \Downarrow\rho'\) | by inversion on \(\mathcal{E}\) |
| \(\mathcal{E_1'} :: \rho \vdash s_1 \Downarrow\rho'''\) | by the i.h. on \(\mathcal{S_1}\) with \(\mathcal{E_1}\) |
| \(\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' }\) | by definition |
Hoare Logic
Semantics
An operational semantics is …
An axiomatic semantics is …
Operational Semantics: Executing Statements
\[ \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' }\)
Assertions
A state assertion is …
A program assertion is …
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\neg\varphi_1 \mid\varphi_1 \Rightarrow\varphi_2 \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: Deductive 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.