
\begin{frame}
\frametitle{}

\vfill
\centerline{\huge Expressing Specifications as Commands}
\vfill

\end{frame}

\begin{frame}
\frametitle{Shorthand: Havoc Multiple Variables at Once}

Variables $V = \{x_1,\ldots,x_n\}$

Translation of $R(havoc(y_1,\ldots,y_m))$:
\pause
\[
    \bigwedge_{v \in V \setminus \{y_1,\ldots,y_m\}} v' = v
\]

Exercise: the resulting formula is the same as for:
\[
   havoc(y_1); \ldots; havoc(y_m)
\]
Thus, the order of distinct havoc-s does not matter.

\end{frame}

\begin{frame}
\frametitle{Programs and Specs are Relations}

\[
\begin{array}{rc}
\mbox{program:} & x = x + 2; y = x + 10 \\
\mbox{relation:} & \{ (x,y,z,x',y',z') \mid x' = x + 2 \land y' = x + 12 \land z' = z \} \\
\mbox{formula:} & x' = x + 2 \land y' = x + 12 \land z' = z
\end{array}
\]
Specification:
\[
    z' = z \land (x > 0 \rightarrow (x' > 0 \land y' > 0)
\]
Adhering to specification is relation subset:
\[
\begin{array}{rl}
          & \{ (x,y,z,x',y',z') \mid x' = x + 2 \land y' = x + 12 \land z' = z \}  \\
\subseteq & \{ (x,y,z,x',y',z') \mid z' = z \land (x > 0 \rightarrow (x' > 0 \land y' > 0)) \}
\end{array}
\]
Non-deterministic programs are a way of writing specifications
\end{frame}


\begin{frame}
\frametitle{Writing Specs Using Havoc and Assume: Examples}

Program variables $V = \{ x, y, z \}$

Formula for relation (talks only about resulting state):
\[
   z' = z \land x' > 0 \land y' > 0
\]
Corresponding program: \pause
\[
    havoc(x,y); assume(x > 0 \land y > 0)
\]
\pause
Formula for relation:
\[
   z' = z \land x' > x \land y' > y
\]
Corresponding program? \pause

Use local variables to store initial values. \pause

\lstinputlisting{spechavoc.scala}

\end{frame}

\begin{frame}
\frametitle{Writing Specs Using Havoc and Assume}

Global variables $V = \{x_1,\ldots,x_n\}$

Specification
\[
   F(x_1,\ldots,x_n,x'_1,\ldots,x'_n)
\]
Becomes \pause

\[\{\begin{array}[t]{l}
   var\ y_1,\ldots,y_n;\\
   y_1 = x_1; \ldots; y_n = x_n; \\
   havoc(x_1,\ldots,x_n); \\
   assume(F(y_1,\ldots,y_n,x_1,\ldots,x_n)) \ \}
\end{array}\]

\end{frame}

\begin{frame}
\frametitle{Program Refinement and Equivalence}

For two programs, define \textbf{refinement} $P_1 \sqsubseteq P_2$ iff 
\[
    R(P_1) \rightarrow R(P_2)
\]
is a valid formula. 

(Some books use the opposite meaning of $\sqsubseteq$.)

As usual, $P_2 \sqsupseteq P_1$ iff $P_1 \sqsubseteq P_2$. 
\begin{itemize}
\item $P_1 \sqsubseteq P_2$ iff $\rho(P_1) \subseteq \rho(P_2)$
\end{itemize}
Define \textbf{equivalence} 
$P_1 \equiv P_2$ iff $P_1 \sqsubseteq P_2 \land P_2 \sqsubseteq P_1$
\begin{itemize}
\item $P_1 \equiv P_2$ iff $\rho(P_1) = \rho(P_2)$
\end{itemize}


Example for $V = \{ x,y\}$
\[
    \{ var\ x0; x0= x; havoc(x); assume(x > x0) \}  \sqsupseteq (x = x + 1)
\]
Proof: Use $R$ to compute formulas for both sides and simplify. \pause
\[
    x' = x + 1 \land y'=y \ \rightarrow\ x' > x \land y'=y
\]

\end{frame}


\begin{frame}
\frametitle{Stepwise Refinement Methodology}

Start form a possibly non-deterministic specification $P_0$

Refine the program until it becomes deterministic and efficiently executable.
\[
   P_0 \sqsupseteq P_1 \sqsupseteq \ldots \sqsupseteq P_n
\]

Example:
\[\begin{array}{rl}
            & havoc(x); assume(x > 0); havoc(y); assume(x < y) \\
\sqsupseteq & havoc(x); assume(x > 0); y = x + 1 \\
\sqsupseteq & x = 42; y = x + 1  \\
\sqsupseteq & x = 42; y = 43
\end{array}\]
In the last step program equivalence holds as well

\end{frame}


\begin{frame}
\frametitle{Monotonicity with Respect to Refinement}


Theorem: if $P_1 \sqsubseteq P_2$ then $(P_1;P) \sqsubseteq (P_2;P)$ 

\pause
Version for relations:
$
   (p_1 \subseteq p_2) \rightarrow (p_1 \circ p) \subseteq (p_2 \circ p)
$

\ \\

\pause
Theorem: if $P_1 \sqsubseteq P_2$ then $(P;P_1) \sqsubseteq (P;P_2)$

\pause
Version for relations:
$
   (p_1 \subseteq p_2) \rightarrow (p \circ p_1) \subseteq (p \circ p_2)
$

\ \\

Theorem: if $P_1 \sqsubseteq P_2$ and $Q_1 \sqsubseteq Q_2$ then
\[
    (if\ (*) P_1\ else\ Q_1) \sqsubseteq  (if\ (*) P_2\ else\ Q_2)
\]
\pause
Version for relations:
$
   (p_1 \subseteq p_2) \land (q_1 \subseteq q_2) \ \ \rightarrow\ \
   (p_1 \cup q_1) \subseteq (p_2 \cup q_2)
$


\end{frame}
