Collecting Semantics
What questions do you have? What questions does your neighbor have?
Questions?
Review: Fixed Points
Fixed Points
\[ \begin{array}{rcl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack & = & \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack\mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot \\ \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack & = & F_{\mathbf{while}\texttt{(}e\texttt{)}s}(\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack) \\ F_{\mathbf{while}\texttt{(}e\texttt{)}s} & \mathrel{:=}& \lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot \end{array} \]
We want to pick a specific fixed point of \(F_{\mathbf{while}\texttt{(}e\texttt{)}s}\).
Ordering Transformers
Order store transfomers by most “don’t know yet”.
\[ \begin{array}{rcl} f_1 \sqsubseteq f_2 & \text{iff} & \text{$f_1(\mathring{\rho}) = \bot$ or $f_1(\mathring{\rho}) = f_2(\mathring{\rho})$} \quad\text{for all $\mathring{\rho}$} \end{array} \]
Fixed-Point Theorems
Theorem 1 (Kleene Fixed-Point Theorem) Let \(P\) be a complete partial order and \(k : P \rightarrow P\) be a continuous function. Then, \(k\) has a least fixed point that can be computed as follows: \[ \begin{array}{rcl} \operatorname{lfp}\,k & = & \bigsqcup_i k^i(\bot) \end{array} \]
Theorem 2 (Tarski-Knaster Fixed-Point Theorem) Let \(L\) be a complete lattice and \(m : L \rightarrow L\) be a monotone function. Then, \(m\) has a least fixed point.
Denotational Semantics: While: Fixed Points
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack = \lambda \mathring{\rho}.\mathring{\rho}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack s \rbrack\!\rbrack & \mathrel{:=}& \lambda \bot.\bot \\ \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho \\ \lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \lbrack\!\lbrack s_2 \rbrack\!\rbrack\, (\lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho) \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho \,\operatorname{else}\, \lbrack\!\lbrack s_2 \rbrack\!\rbrack\,\rho \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho ) \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack & \mathrel{:=}& \operatorname{lfp}\,(\lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot ) \end{array} \]
Denotational Semantics: While with While
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack = \lambda \mathring{\rho}.\mathring{\rho}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack & \mathrel{:=}& \operatorname{lfp}\,(\lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot ) \end{array} \]
\[ \text{or} \]
\[ \begin{array}{l} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack \quad \mathrel{:=} \\ \qquad\operatorname{let}\,F = (\lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot ); \\ \qquad f \leftarrow \bot; f' \leftarrow F\,f; \operatorname{while}\, \neg(f' \sqsubseteq f) \,\operatorname{do}\, \{ f \leftarrow f'; f' \leftarrow F\,f; \} ; \\ \qquad f \end{array} \]
Collecting Semantics
Them’s Just Semantics
An operational semantics is …
An axiomatic semantics is …
A denotational semantics is …
A collecting semantics is …
Them’s Just Semantics
An operational semantics is an interpreter.
An axiomatic semantics is an verifier.
A denotational semantics is a compiler.
A collecting semantics is an exhaustive tester.
Verification as Reachability
We want to collect all reachable states — properties.
\[ \begin{array}{rr} \text{store properties} & P& \mathrel{::=}& \circ\mid P,\rho \end{array} \]
That is, we want to define a collecting semantics \(\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'\) for the forward state-reachability property. That is, we want the following equation to hold:
\[ \lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace{P} = \{ \rho' \mid \text{$\rho \vdash s \Downarrow\rho'$ for all $\rho\in P$} \} \]
Exercise: State-Collecting Semantics
Define \(\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'\) by induction on the structure of statement \(s\). You may assume a denotation for expressions \(\lbrack\!\lbrack e \rbrack\!\rbrack = \lambda \rho.v\).
State-Collecting Semantics
\[ \begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \cdots \mid\mathbf{assume}\;e \\ \text{store-property transformers} & f& \mathrel{::=}& \lambda P.P' \end{array} \]
\[ \fbox{$\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'$} \]
\[ \begin{array}{rrl} \lbrace\!\lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. P \\ \lbrace\!\lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lbrace\!\lbrack\!\lbrack s_2 \rbrack\!\rbrack\!\rbrace \circ \lbrace\!\lbrack\!\lbrack s_1 \rbrack\!\rbrack\!\rbrace \\ \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \{ \rho \mid \text{$\lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}$ for all $\rho\in P$} \} \\ \lbrace\!\lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack\!\rbrace\,P \cup \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;\texttt{!}{e} \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack\!\rbrace\,P \\ \lbrace\!\lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \{ \rho(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho ) \mid \rho\in P \} \\ \\ \lbrace\!\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P. \lbrace\!\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack\!\rbrace\left( \bigcup_i (\lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack\!\rbrace)^i\,P \right) \\ & \text{or} & \\ \lbrace\!\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack\!\rbrace & \mathrel{:=}& \lambda P.\lbrace\!\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack\!\rbrace\left( \operatorname{lfp}\,(\lambda P'. P \cup \lbrace\!\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack\!\rbrace\,P' ) \right) \end{array} \]