\begin{frame}
  \frametitle{Replacing Calls by Contracts: Example}

\small
  
\begin{minipage}{6cm}
  \lstinputlisting{mutualrec1.scala}
\end{minipage}
\begin{minipage}{4cm}
  \lstinputlisting{mutualrec2.scala}
\end{minipage}

\pause Reduces to checking these two non-recursive procedures:

\begin{minipage}{6cm}
  \lstinputlisting{mutualrec1h.scala}
\end{minipage}
\begin{minipage}{4cm}
  \lstinputlisting{mutualrec2h.scala}
\end{minipage}
\end{frame}

\begin{frame}
\frametitle{Reminder: Loop-Free Programs as Relations}

\[\begin{array}{r|c|l}
   \mbox{command } c  & R(c) & \rho(c) \\\hline\hline
  (x=t)               & x' = t \land \bigwedge_{v \in V \setminus \{x\}} v' = v 
                      & \\
  \semic{c_1}{c_2}    & \exists \bar z.\ \ 
                         R(c_1)[\bar x' := \bar z] \land R(c_2)[\bar x := \bar z]
                      & \rho(c_1) \circ \rho(c_2) \\
  \ifstar{c_1}{c_2}  & R(c_1) \lor R(c_2) & \rho(c_1) \cup \rho(c_2) \\
  \mathbf{assume(F)} & F \land \bigwedge_{v \in V} v'=v & \Delta_{S(F)} 
\end{array}
\]

$\rho(x_i=t) = \{ ((x_1,\ldots,x_i,\ldots,x_n),(x_1,\ldots,x_i',\ldots,x_n) \mid x'_i = t \}$

$S(F) = \{ \bar x \mid F \}$, \ \ $\Delta_A = \{ (\bar x, \bar x) \mid \bar x \in A \}$
(diagonal relation on $A$)

$\Delta$ (without subscript) is identity on entire set of states (no-op)

We always have: $\rho(c) = \{ (\bar x, \bar x') \mid R(c) \}$ 

Shorthands:
\[\begin{array}{c|c}
   \ifstar{c_1}{c_2}   &  \ndchoice{c_1}{c_2}   \\\hline
   \mathbf{assume}(F) & [F] 
\end{array}\]
Examples:
\[\begin{array}{l}
  \ifcond{F}{c_1}{c_2} 
  \ \ \equiv \ \
  { [F];c_1 \ \choiceop \ [\lnot F];c_2 } \\
  \ifcondskip{F}{c}
  \ \ \equiv \ \ 
  { [F];c \ \choiceop \ [\lnot F] } \\
\end{array}\]
\end{frame}
