\documentclass{article}
\sloppy

\usepackage{amsmath}
\usepackage{amsthm}

\title{Model Checking (IN2050): Exercise 1\\
  Proving Correctness
}
\author{Andrey Rybalchenko}
\begin{document}
\maketitle

\newcommand{\lneg}{\neg}
\newcommand{\ltrue}{\mathit{true}}
\newcommand{\lfalse}{\mathit{false}}
\newcommand{\setOf}[1]{\{#1\}}

\newtheorem{theorem}{Theorem}

\begin{abstract} 
%
We present a basic algorithm that computes the set of nodes reachable
in a (finite) graph.
For this algorithm we formulate the corresponding correctness
properties and present their proofs.
\end{abstract}

\section{Reachability algorithm}

\begin{figure}[h]
  \hrule
  \centering
  \begin{minipage}[t]{.8\linewidth}
\begin{verbatim}

algorithm BRA
input
  N : set of nodes
  n0 : start node, where n0 \in N
  E : set of edges, where E \subseteq N \times N
var
  C : nodes reached so far
  done : Boolean flag
  D : auxiliary set of nodes
begin
  C := {n0}
  done := false
  while \neg done do
    D := { d \in N | \exists c \in C: (c, d) \in E }
    if \neg (D \subseteq C) then
      C := C \cup D
    else 
      done := true
  od
  return C
end.  

\end{verbatim}
  \end{minipage}
  \hrule
  \caption{A basic algorithm BRA for computing reachable nodes in a (finite) graph.}
  \label{fig-alg}
\end{figure}

Figure~\ref{fig-alg} presents an algorithm BRA that computes graph
nodes that are reachable from the start node by traversing the graph
edges.

\section{Properties and proofs}

\subsection{Termination}

\begin{theorem}
  BRA terminates on finite graphs.
\end{theorem}
\begin{proof}
%

\subsubsection*{Ordering}
We define an ordering on pairs of integer numbers as follows.
%
\begin{equation*}
  (a, b) > (a', b') : \quad a > a' \lor a = a' \land b > b'
\end{equation*}
%
Then $(a, b) \geq (a', b')$ if either $(a, b) = (a', b')$ or $(a, b) >
(a', b')$.

\subsubsection*{Ranking function}

Given a finite set $X$, let $|X|$ be its size.
Next, we define a ranking function $r$ from the values of \verb|C| and
\verb|done| to pairs of integer numbers as follows, which is possible
since both $\verb|N|$ and $\verb|C|$ are finite.
%
\begin{equation*}
  r(\verb|C|, \verb|done|) :\quad 
  (|\verb|N||-|\verb|C||, \textbf{if } \verb|done| \textbf{ then } 0 \textbf{ else } 1)
\end{equation*}
%
For example, for $\verb|N| = \setOf{1,2,3}$ we have
%
\begin{equation*}
  \begin{array}[t]{l@{\;=\;}l}
    r(\setOf{1}, \lfalse) & (2, 1)\ ,\\
    r(\setOf{1,2}, \lfalse) & (1, 1)\ ,\\
    r(\setOf{1,2,3}, \ltrue ) & (0, 0)\ .
  \end{array}
\end{equation*}
%

\subsubsection*{Ranking decrease}

Now we show that the value of the ranking function decreases during
each loop iteration.

First, we consider the path through the loop that traverses the if
branch of the conditional statement.
The corresponding proof obligation is
%
\begin{equation*}
  r(\verb|C|, \lfalse) > r(\verb|C| \cup \verb|D|, \lfalse )\ ,
\end{equation*}
%
under the assumption that $\neg(\verb|D|\subseteq \verb|C|)$.
This assumption implies that there exists a node $\verb|d| \in
\verb|D|$ such that $\verb|d| \not\in \verb|C|$.
Hence, $|\verb|C|| < |\verb|C| \cup \verb|D||$.
 which proves the
obligation.

Second, we consider the path that traverses the else branch.
Since the set $\verb|C|$ does not change, we immediately obtain
%
\begin{equation*}
  r(\verb|C|, \lfalse) > r(\verb|C|, \ltrue )\ .
\end{equation*}
%

\subsubsection*{Ranking bound}

We prove that an iteration of the loop can only take place if the
algorithm state satisfies the following condition.
%
\begin{equation*}
  r(\verb|C|, \verb|done|) \geq (0, 0)
\end{equation*}
%
This statement follows from the fact that the algorithm maintains the
relation $\verb|C| \subseteq \verb|N|$ and the loop condition.

\subsubsection*{Putting everything together}

First, we observe that there is no infinite chain of pairs of integers
$(a_0, b_0) > (a_1, b_1) > \dots$ such that for each $i\geq 0$ we
have~$(a_i, b_i) \geq (0, 0)$.
Together with the ranking decrease and ranking bound statements this
observation implies termination of the algorithm.
%
\end{proof}

\subsection{Reachability}

\begin{theorem}
% 
Each node $\verb|c|$ in the set $\verb|C|$ computed by BRA is
reachable from $\verb|n0|$ by following edges from $\verb|E|$.
Formally,
% 
\begin{equation*}
  \forall \verb|c| \in \verb|C|: (\verb|n0|, \verb|c|) \in \verb|E|^*\ .
\end{equation*}
% 
\end{theorem}
\begin{proof} 
%
We prove the theorem by induction on the number of the loop
iterations~$k$.
Our induction hypothesis $\mathit{Hyp}(k)$ is:
%
\begin{quote} 
%
Each node $\verb|c|$ that was added to $\verb|C|$ at the iteration
$k'$ such that $k' \leq k$ is reachable, i.e., $(\verb|n0|, \verb|c|)
\in \verb|E|^*$.
\end{quote}
%

\subsubsection*{Base case}

For $k=0$, we have $\verb|C| = \setOf{\texttt{n0}}$.
Since $(\verb|n0|, \verb|n0|) \in \verb|E|^*$, $\mathit{Hyp}(0)$
holds.

\subsubsection*{Step}
 
We assume that for $k$ the induction hypothesis $\mathit{Hyp}(k)$
holds, i.e., each node $\verb|c|$ added to $\verb|C|$ at the iteration
$k'$ such that $k' \leq k$ is reachable, i.e., $(\verb|n0|, \verb|c|)
\in \verb|E|^*$.
We prove~$\mathit{Hyp}(k+1)$, which amounts to proving that $\verb|D|$
computed during the $k+1$th interaction by following the if branch is
reachable.
The case when the $k+1$th iteration goes through the else branch does
not modify $\verb|C|$ and hence $\mathit{Hyp}(k+1)$ holds.

By the induction hypothesis, for each $\verb|d|\in\verb|D|$ there
exists $\verb|c|\in\verb|C|$ at step $k$ such that
$(\verb|c|,\verb|d|)\in \verb|E|$ and $\verb|c|$ is reachable, i.e.,
$(\verb|n0|, \verb|c|)\in \verb|E|^*$.
The induction step follows immediately.
%
\end{proof}
%

\clearpage
\appendix
\section{Notation}
\begin{table}[h]
  \centering
  \begin{tabular}[t]{l|c|l|l}
    English & math & ASCII & example \\ \hline\hline
    element of & $\in$ & \verb|\in| & $1\in \setOf{1,2,3}$\\ 
    subset of & $\subseteq$ & \verb|\subseteq| & $\setOf{1,2}\subseteq \setOf{1,2,3}$\\
    union of & $\cup$ & \verb|\cup| & $\setOf{1,2} \cup \setOf{2,3} = \setOf{1,2,3}$\\
    intersection of & $\cap$ & \verb|\cap| & $\setOf{1,2} \cap \setOf{2,3} = \setOf{2}$\\
    subtraction of &  $\setminus$ & \verb|\setminus| & $\setOf{1,2} \setminus \setOf{2,3} = \setOf{1}$\\
    Cartesian product & $\times$ & \verb|\times| & $\setOf{1,2} \times \setOf{2,3} = \setOf{(1,2),(1,3), (2,2), (2,3)}$\\
    exists & $\exists$ & \verb|\exists| \\
    forall & $\forall$ & \verb|\forall| \\
    negation & $\lneg$ & \verb|\lneg| \\
    conjunction & $\land$ & \verb|\land| \\
    disjunction & $\lor$ & \verb|\lor| \\
  \end{tabular}
  \caption{Mathematical symbols in ASCII.}
  \label{tab-math-ascii}
\end{table}


\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
