\begin{frame}
\titleslide{About Strength and Weakness}
\end{frame}

\begin{frame}
\frametitle{Putting Conditions on Sets Makes them Smaller}

Let $P_1$ and $P_2$ be formulas (``conditions'') whose free variables are among $\bar x$.
Those variables may denote program state.

When we say ``condition $P_1$ is stronger than condition $P_2$'' it simply means 
\centerline{$   \forall \bar x.\ (P_1 \rightarrow P_2)$}

\begin{itemize}
\item if we know $P_1$, we immediately get (conclude) $P_2$
\item if we know $P_2$ we need not be able to conclude $P_1$ 
\end{itemize}

\ \\

Stronger condition = smaller set: if $P_1$ is stronger than $P_2$ then
\centerline{$\{ \bar x \mid P_1 \} \subseteq \{ \bar x \mid P_2 \}$}

\begin{itemize}
\item strongest possible condition: ``false'' $\leadsto$ smallest set: $\emptyset$
\item weakest condition: ``true'' $\leadsto$ biggest set: set of all tuples
\end{itemize}
\end{frame}

\begin{frame}
\titleslide{Hoare Triples}
\end{frame}

% =======================================================================
\begin{frame}
 \frametitle{Hoare Logic Example}
 {\small
 We have seen how to translate programs into relations. We can use these relations 
 in a proof system called Hoare logic.
 Hoare logic is a way of inserting annotations into code to make proofs about
  (imperative) program behavior simpler.}\\
 \begin{minipage}{4cm}
  Example proof:
 \end{minipage}
 \begin{minipage}{4cm}
 %\lstset{commentstyle=\codestyle\color{gray}}
\lstinputlisting{hoare_proof.scala}
\end{minipage}
\end{frame}

\begin{frame}
\frametitle{Hoare Triple Definitions}

\begin{tabular}{@{}ccc}
\begin{minipage}{3.3cm}
$P, Q \subseteq S$ \ \ \ \ $r \subseteq S \times S$

\textbf{Hoare Triple:}
\end{minipage}
&
\includegraphics[scale=0.35]{tony.png}
&
\begin{minipage}{8cm}
  {\footnotesize from Wikipedia page \textsl{Tony Hoare}} \\
  {\footnotesize \url{http://slideshot.epfl.ch/play/suri_hoare}} \\
  \

  \

  \
\end{minipage}
\end{tabular}

\vspace*{-0.5cm}
\[
    \{P \}\ r\ \{ Q \} \iff
    \forall s,s' \in S. \left( s \in P \land (s,s') \in r \rightarrow s' \in Q \right)
\]
($\{P\}$ and $\{Q\}$ do not denote singleton sets, they are just
notation for assertions)

\textbf{Strongest postcondition:}
\[
   sp(P,r) = \{ s' \mid \exists s.\, s \in P \land (s,s') \in r \}
\]
\textbf{Weakest precondition:}
\[
   wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \}
\]
\end{frame}

\begin{frame}
 \frametitle{Postconditions and Their Strength}
 
 What is the relationship between these postconditions?\\
 \[
  \{x = 5\} \quad x := x + 2 \quad \{{\bf x > 0}\}
 \]
 \[
  \{x = 5\} \quad x := x + 2 \quad \{{\bf x = 7}\}  
 \]

\pause
\begin{itemize}
\item weakest conditions (predicates) correspond to largest sets
\item strongest conditions (predicates) correspond to smallest sets
\end{itemize}
 that satisfy a given property.\\
 \vspace{10pt}
  (Graphically, a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas 
  a weaker condition $x > 0$ denotes the entire half-plane.)

\end{frame}

\begin{frame}
 \frametitle{Strongest Postcondition}
 Definition: For $P \subseteq S$, $r \subseteq S\times S$,
\[
   sp(P,r) = \{ s' \mid \exists s. s \in P \land (s,s') \in r \}
\]

This is simply the relation image of a set.
 
 \begin{center}
 \includegraphics[width=0.6\textwidth]{sp.png}
\end{center}
\end{frame}

\begin{frame}
 \frametitle{Weakest Precondition}
Definition: for $Q \subseteq S$, $r \subseteq S \times S$,
\[
   wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \}
\]

Note that this is in general not the same as $sp(Q,r^{-1})$ when the relation is non-deterministic or partial.
\begin{center}
 \includegraphics[width=0.6\textwidth]{wp.png}
\end{center}
\end{frame}


\begin{frame}
 \frametitle{Three Forms of Hoare Triple}

Lemma: the following three conditions are equivalent:
\begin{itemize}
 \item $\{P\} r \{Q\}$
 \item $P \subseteq wp(r,Q)$
 \item $sp(P,r) \subseteq Q$ 
\end{itemize}
\pause
Proof. The three conditions expand into the following three formulas
\begin{itemize}
 \item $\forall s,s'.\ [(s \in P \land (s,s') \in r) \rightarrow s' \in Q]$
 \item $\forall s.\ [s \in P \rightarrow (\forall s'. (s,s') \in r \rightarrow s' \in Q)]$
 \item $\forall s'.\ [(\exists s.\ s \in P \land (s,s') \in r) \rightarrow s' \in Q]$
\end{itemize}
which are easy to show equivalent using basic first-order logic properties, such as
$(P \land Q \longrightarrow R) \longleftrightarrow (P \longrightarrow (Q \longrightarrow R))$,
$(\forall u. (A \longrightarrow B)) \longleftrightarrow (A \longrightarrow \forall u.B)$ when
$u \notin FV(A)$, and
$(\forall u. (A \longrightarrow B)) \longleftrightarrow ((\exists u.A) \longrightarrow B)$ when
$u \notin FV(B)$.

\end{frame}
