Abstract Transition Semantics

Bor-Yuh Evan Chang

Tuesday, November 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 23 - 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:

r = 1;
while
  (n > 0) {
    r = r * x;
    n = n - 1;
  }
  

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