Abstract Transition Semantics
What questions do you have? What questions does your neighbor have?
Announcements
November 2025
Su Mo Tu We Th Fr Sa
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30
December 2025
Su Mo Tu We Th Fr Sa
1 2 3 4 5 6
7 8 9 10 11 12 13 - Thanksgiving - November 24-28
- Presentations - Monday, December 8 1:30-4:00
- End of Semester - Friday, December 12
Questions?
Widening
Review: Abstract Interpretation of While
But what’s unsatisfying about the abstract interpretation of \(\mathbf{while}\)?
\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}. \lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \bigsqcup_i (\lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp)^i\,P \right) \\ & \text{or} & \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}.\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \operatorname{lfp}\,(\lambda \hat{\rho}'. \hat{\rho} \mathbin{\sqcup} \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\rho}' ) \right) \end{array} \]
Review: Enforcing Convergence with the Widening Operator
\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack^\sharp & \mathrel{:=}& \lambda \hat{\rho}.\lbrack\!\lbrack\mathbf{assume}\;\texttt{!}{e} \rbrack\!\rbrack^\sharp\left( \operatorname{lfp}\,(\lambda \hat{\rho}'. \hat{\rho} \mathbin{\nabla} \lbrack\!\lbrack \mathbf{assume}\;e \mathbin{\texttt{;}} s_1 \rbrack\!\rbrack^\sharp\,\hat{\rho}' ) \right) \end{array} \]
Review: Widening
Definition 1 (Widening Operator) A widening is an upper-bound operator that enforces convergence:
- upper-bound
- For all \(\hat{\rho}_1, \hat{\rho}_2\), we have that \(\hat{\rho}_1 \mathrel{\sqsubseteq} \hat{\rho}_1 \mathbin{\nabla}\hat{\rho}_2 \) and \(\hat{\rho}_2 \mathrel{\sqsubseteq} \hat{\rho}_1 \mathbin{\nabla}\hat{\rho}_2 \)
- convergence
- For all chains \(\hat{\rho}_0 \mathrel{\sqsubseteq}\hat{\rho}_1 \mathrel{\sqsubseteq}\cdots\), the chain \(\hat{\rho}_0' \mathrel{\sqsubseteq}\hat{\rho}_1' \mathrel{\sqsubseteq}\cdots\) s.t \(\hat{\rho}_0' = \hat{\rho}_0\) and \(\hat{\rho}_i' = \hat{\rho}_{i-1}' \mathbin{\nabla}\hat{\rho}_i\) converges (i.e., there is some \(n\) where \(\hat{\rho}_i' = \hat{\rho}_n'\) for all \(i \geq n\)).
Exercise: Widening for the Interval Domain
Define a widening operator \(\mathbin{\nabla}\) for the interval abstract domain:
\[ \begin{array}{rrrl} \text{abstract numbers} & \hat{n}& \mathrel{::=}& \bot \mid r\mid\top \\ \text{intervals} & r& \mathrel{::=}& (-\infty, n_2] \mid[n_1, n_2] \mid[n_1, \infty) \end{array} \]
Widening for the Interval Domain
\[ \begin{array}{rrll} [n_1, n_2] \mathbin{\nabla}[n_1', n_2'] & \mathrel{:=}& [n_1, \infty) & \text{if $n_1 \leq n_1'$ and $n_2 < n_2'$} \\ [n_1, n_2] \mathbin{\nabla}[n_1', n_2'] & \mathrel{:=}& (-\infty, n_2] & \text{if $n_1 > n_1'$ and $n_2 \geq n_2'$} \\ [n_1, n_2] \mathbin{\nabla}[n_1', n_2'] & \mathrel{:=}& \top & \text{if $n_1 > n_1'$ and $n_2 < n_2'$} \\ \hat{n}_1 \mathbin{\nabla}\hat{n}_2 & \mathrel{:=}& \hat{n}_1 \mathbin{\sqcup}\hat{n}_2 & \text{otherwise} \end{array} \]
Abstract Transition Semantics
JavaScripty Commands and Transitions
\[ \begin{array}{rrrl} \text{commands} & c& \mathrel{::=}& \texttt{;} \mid x \mathrel{\texttt{=}}e \mid\mathbf{assume}\;e \mid c_1 \mathbin{\texttt{;}} c_2 \\ \\ \text{transitions (i.e., control-flow edges)} & t& \mathrel{::=}& \ell_1 \mathrel{\mathord{-}\mkern-4mu[c]\mkern-4mu\mathord{\rightarrow}} \ell_2 \\ \text{locations (i.e., control-flow nodes)} & \ell \\ \\ \text{programs or procedures (i.e., control-flow graphs)} & g& \mathrel{::=}& \circ \mid g,t \end{array} \]
A control-flow graph is a set of a control-flow edges labeled with commands between control locations or program points.
A sequence of atomic commands (i.e., no sequencing or other control-flow) is sometimes called a basic block. A control-flow graph is also often drawn as a flowchart with flow edges between basic-block nodes.
Exercise: Compiling to Control-Flow Graphs
Compile the following example program (for computing \(\texttt{x}^\texttt{n}\)) to a control-flow graph using the line numbers as control-flow locations:
Exercise: Transition Systems
\[ \text{(control-flow) state} \quad \sigma\quad \mathrel{::=}\quad \ell\colon \rho \]
Define the judgment form \(\sigma \rightarrow_{g} \sigma'\) that says, “Control-flow state \(\sigma\) steps to state \(\sigma'\) in program \(g\).”
Transition Systems
\[ \fbox{$\sigma \rightarrow_{g} \sigma'$} \]
\(\inferrule[DoTransition]{ \rho \vdash c \Downarrow\rho' \and \ell \mathrel{\mathord{-}\mkern-4mu[c]\mkern-4mu\mathord{\rightarrow}} \ell' \in g }{ \ell\colon \rho \rightarrow_{g} \ell'\colon \rho' }\)