\begin{frame}
\frametitle{Semantics of a Program with a Loop}

Compute and simplify relation for this program:

\begin{minipage}{4cm}
\lstinputlisting{loop2.scala}
\end{minipage}
\begin{minipage}{4cm}
\[\begin{array}{l}
\rho(x=0) \circ \\
(\Delta_{\pset{y > 0}} \circ \rho(x = x + y; y = y - 1))^* \circ \\
\Delta_{\pset{y \le 0}} \\
\ \\
\end{array}\]
\end{minipage}

\vspace*{-2ex}
\tiny
\[\begin{array}{r|l}
R(x=0) & x'=0 \land y'=y  \\  
R([y > 0]) & y' > 0 \land x'=x \land y'=y  \\
R([y \le 0]) & y' \le 0 \land x'=x \land y'=y  \\ \hline
% ========= One step
R(\begin{array}[t]{l} \relax
  [y > 0];\relax \\
  x = x + y; \\
  y = y - 1) \\
\end{array} &
\begin{array}[t]{l} 
  \ \\
  \ \\
  y > 0 \land x' = x + y \land y' = y - 1
\end{array} \\ \hline
% ========= Many steps
R((\begin{array}[t]{l} \relax
  [y > 0];\relax \\
  x = x + y; \\
  y = y - 1)^k), k>0 \\
\end{array} &
\begin{array}[t]{l} 
  \ \\
  y-(k-1) > 0 \land \\
  x' = x + (y + (y{-}1) + \cdots + y-(k{-}1)) \land y' = y - k
\end{array} \\ 
\begin{array}[t]{l} \relax
  \ \\
 \ \\
\end{array} &
\begin{array}[t]{l} 
 \mbox{\emph{i.e.}} \ \\
 y \ge k \land 
 x' = x + k(y + y-(k{-}1))/2 \land y' = y - k
\end{array} \\ \hline
% Transitive closure
R((\begin{array}[t]{l} \relax
  [y > 0];\relax \\
  x = x + y; \\
  y = y - 1)^*) \\
\end{array} &
\begin{array}[t]{l}
 (x'=x \land y'=y)\ \lor \ \ 
 \exists k > 0.\  y \ge k \land x' = x + k(2y-k + 1))/2 \land y' = y - k
\end{array} \\ 
\begin{array}[t]{l} \relax
  \ \\
\end{array} &
\begin{array}[t]{l} 
 \hspace{-1em}\mbox{\emph{i.e.}, eliminating }\ k = y-y', \ \\
 \ (x'=x \land y'=y) \lor \big(y-y'>0 \land 
 y' \ge 0 \land x' = x + (y-y')(y + y' + 1)/2\big) \\
%\hspace{-1em} \mbox{\emph{i.e.}} \ \ 
%   \mathbf{y-y' \ge 0} \land y' \ge 0 \land x' = x + (y-y')(y + y' + 1)/2
\end{array} \\ \hline
% Final result
R(\mbox{program}) &
  (x'=0 \land y'=y \land y' \le 0) \lor
  \big(y > 0 \land y' = 0 \land x' = y(y + 1)/2\big) 
\end{array}\]

\end{frame}

\begin{frame}
  \frametitle{Remarks on Previous Solution}

Intermediate components can be more complex than final result
\begin{itemize}
\item they must account for all possible initial states, even those
  never reached in actual executions
\end{itemize}

\ \\

Be careful with handling base case. The following solution:
\[
y' = 0 \land x' = y(y + 1)/2
\]
is ``almost correct'': it
incorrectly describes behavior when the initial state has, for example, $y=-2$

\end{frame}

\begin{frame}
\frametitle{Approximate Semantics of Loops}

Instead of computing exact semantics, it can be sufficient to compute approximate semantics.
Observation: $r_1 \subseteq r_2 \rightarrow r_1^* \subseteq r_2^*$ (monotonicity still holds).

Suppose we only wish to show that the semantics is included in $s = \{(x,y,x',y') \mid y' \le y\}$.
Note $s \circ s \subseteq s$, $s^* \subseteq s$. Then

\begin{minipage}{5cm}
\lstinputlisting{loop2.scala}
\end{minipage}
\begin{minipage}{4cm}
\[\begin{array}{l}
\rho(x=0) \circ \\
(\Delta_{\pset{y > 0}} \circ \rho(x = x + y; y = y - 1))^* \circ 
\Delta_{\pset{y \le 0}} \\
\ \\
\end{array}\]
\end{minipage}

\pause

\begin{minipage}{5cm}
  \centering
 \Large
 \rotatebox[origin=c]{270}{$\sqsubseteq$} 
\end{minipage}
\begin{minipage}{4cm}
  \centering
  \Large
 \rotatebox[origin=c]{270}{$\subseteq$} 
\end{minipage}

\pause

\begin{minipage}{5cm}
  \lstinputlisting{loop2approx.scala}
  \vfill\vfill
\end{minipage}
\begin{minipage}{4cm}
\[\begin{array}{l}
s\ \circ \\
(s \circ s \circ s)^* \circ s
\end{array}\]
\centering {\Large \rotatebox[origin=c]{270}{$\subseteq$}}
\[
   s  
\]
\end{minipage}

\end{frame}


%\end{document}
