%% LyX 1.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[american]{amsbook}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\setlength\parskip{\smallskipamount}
\setlength\parindent{0pt}
\usepackage{amssymb}
\IfFileExists{url.sty}{\usepackage{url}}
                      {\newcommand{\url}{\texttt}}

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 \numberwithin{section}{chapter}
 \theoremstyle{plain}    
 \newtheorem{thm}{Theorem}[section]
 \numberwithin{equation}{section} %% Comment out for sequentially-numbered
 \numberwithin{figure}{section} %% Comment out for sequentially-numbered
 \theoremstyle{definition}
 \newtheorem*{defn*}{Définition}
 \newenvironment{lyxcode}
   {\begin{list}{}{
     \setlength{\rightmargin}{\leftmargin}
     \setlength{\listparindent}{0pt}% needed for AMS classes
     \raggedright
     \setlength{\itemsep}{0pt}
     \setlength{\parsep}{0pt}
     \normalfont\ttfamily}%
    \item[]}
   {\end{list}}
 \theoremstyle{definition}
  \newtheorem*{example*}{Exemple}
 \theoremstyle{plain}    
 \newtheorem*{thm*}{Théorème} 
 \theoremstyle{remark}
 \newtheorem*{rem*}{Remarque}
 \theoremstyle{definition}
  \newtheorem{xca}{Exercice}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathbb{C}}
\usepackage{hyperref}

\usepackage[francais,american]{babel}
\makeatother
\begin{document}

\chapter{Proof Of Correctness (Sections 1.6, 2.3)}


\section{Introduction}

\begin{quote}
{}``Beware of bugs in the above code; I have only proved it correct,
not tried it.''

Donald E. Knuth \url{http://www-cs-faculty.stanford.edu/~knuth/}
\end{quote}
How to check if a program is correct ?

Why checking if a program is correct ?

What is a correct program ?

%

%

%

%

%

%

%

%%

\begin{defn*}
\emph{Specification}: precise description of how a program should
behave.

A program is \emph{correct}, if it behaves in accordance with its
specifications.
\end{defn*}
How to check if a program is correct?

\begin{itemize}
\item Testing


Designing good test data sets

You can prove there is a bug. No proof of no bug!

\item Proof of Correctness
\end{itemize}

\section{Correctness}


\subsection{Assertions}

\begin{lyxcode}
~~...

~~x=sqrt(r);~~//~r~should~be~>=~0~!

~~x=a{[}i{]};~~~~~//~i~should~be~in~the~correct~range

~~...


\end{lyxcode}
\begin{defn*}
\emph{Assertion}: condition on the variables of a program that should
be verified at some given step, if the program is running correctly.
\end{defn*}
Using assert in C/C++:

\begin{lyxcode}
\#include~<assert.h>



~~...

~~assert(r>=0);

~~x=sqrt(r);

~~assert((0<=i)~\&\&~(i<MAX));

~~x=a{[}i{]};

~~...
\end{lyxcode}
Each assertion is automatically checked:

\begin{itemize}
\item If the assertion is not verified, the program stops immediately with
a message like:
\end{itemize}
\begin{lyxcode}
Assertion~failed,~line~35~of~file~foo.c
\end{lyxcode}
\begin{itemize}
\item That's more informative for the user than a segmentation fault at
the following line.
\item This can be deactivated by adding a \#define NDEBUG preprocessor directive.
\end{itemize}
With C++, java and other languages, you can use \emph{exceptions}
instead of assert:

\begin{itemize}
\item More informative error messages
\item Error recovery mechanisms
\end{itemize}
Static type checking also makes some kind of assertion checking.

One way or the other, \emph{check assertions in your programs.}


\subsection{Specification of a function:}

\begin{lyxcode}
int~factorial(int~n);

//~Preconditions:~n~is~a~non-negative~integer

//~Postcondition:~returns~n!



...



int~factorial(int~n)~\{

~~assert(n>=0);

~~if~(n==0)~return~1;

~~return~n{*}factorial(n-1);

\}
\end{lyxcode}
The specification of a program can be formalized as follow:

\begin{itemize}
\item $P$: program
\item $X$: input 
\item $P(X)$: output
\item $Q$: precondition: predicate $Q(X)$ on the input
\item $R$: postcondition: predicate $R(X,P(X))$ on the input and the output
\end{itemize}
\begin{example*}
Program to compute of a square root
\end{example*}
\begin{itemize}
\item $P$: \texttt{$y:=\textrm{sqrt}(x);$}
\item $X$: $x$
\item $P(x)$: $y$
\item $Q(x)$: $x\geq0$
\item $R(x,y)$: $y^{2}=x$
\end{itemize}
\begin{defn*}
P is \emph{correct} if $(\forall X)\textrm{ }Q(X)\rightarrow R(X,P(X))$.

A \emph{Hoare triple} is just a short hand notation: \{$Q$\} $P$
\{$R$\}
\end{defn*}
\begin{example*}
\{$x\geq0$\} \texttt{$y:=\textrm{sqrt}(x);$;} \{$y^{2}=x$\}
\end{example*}

\section{Proof of Correctness}


\subsection{Divide and Conquer}

Let P be a big program:

\begin{lyxcode}
$s_{0}$

$s_{1}$

$s_{2}$

...

$s_{n-1}$
\end{lyxcode}
To prove \{$Q$\} $P$ \{$R$\}, we break $P$ into elementary steps,
and insert assertions that describes the state of the program at each
step:

\begin{lyxcode}
\{$Q$\}

$s_{0}$

\{$R_{1}$\}

$s_{1}$

\{$R_{1}$\}

$s_{2}$

...

$s_{n-1}$

\{$R$\}
\end{lyxcode}
$P$ is correct, if each step is correct, i.e. the following Hoare
triples hold:

\begin{itemize}
\item \{$Q$\} $s_{0}$ \{$R_{1}$\}, 
\item \{$R_{1}$\} $s_{1}$ \{$R_{2}$\}, 
\item \ldots{}
\item \{$R_{n-1}$\} $s_{n-1}$ \{$R$\}
\end{itemize}
To prove that the elementary steps are correct, we will use some syntactic
rules, exactly as we did in formal logic.


\subsection{Assignment rule:}

Consider the following Hoare triple: \{$Q$\} $x:=e$ \{$R$\}

\begin{thm*}
If from $Q$ you can derive $R$ with $x$ substituted everywhere
by $e$,

then the Hoare triple is valid.
\end{thm*}
\begin{example*}
\{$x=2$\} \texttt{$y:=x+1$} \{$y=3$\}

When substituting, $y=3$ becomes $x+1=3$.

From $x=2$, you can deduce $x+1=3$.

So this Hoare triple holds.
\end{example*}
%

\begin{example*}
\{$x>0$\} \texttt{$x:=x+1$} \{$x>1$\}

Here it can be confusing. 

The same name $x$ stands for both the value of $x$ before and after
the assignments.

If you get confused, just rename the variable:

\{$x_{0}>0$\} \texttt{$x_{1}:=x_{0}+1$} \{$x_{1}>1$\}

When substituting, $x_{1}>1$ becomes $x_{0}+1>1$, which you can
deduce from $x_{0}>0$.
\end{example*}

\subsection{Conditional Rule}

Consider the following Hoare triple:

\begin{lyxcode}
\{$Q$\}

if~condition~$B$~then

~~$P_{1}$

else

~~$P_{2}$

end~if

\{$R$\}
\end{lyxcode}
\begin{thm*}
If the Hoare triples \{$Q\wedge B$\} $P_{1}$\{$R$\} and \{$Q\wedge B'$\}
$P_{2}$ \{$R$\} hold, 

then the Hoare triple above holds.
\end{thm*}
\begin{example*}
\cite[Exercise~11 p.~78]{Gersting.MSCS}
\end{example*}

\subsection{Loop Rule}

Consider the following Hoare triple:

\begin{lyxcode}
\{$Q$\}

while~condition~$B$~do

~~$P$

end\_while

\{$R$\}
\end{lyxcode}
\{$Q$\} describes the state of the program before the loop.

We need to have a predicate which describes the state of the program
DURING the loop: 

The \emph{loop invariant} \{$S$\}

Most of the time, \{$Q$\} will do the job, but not always.

\begin{thm*}
If the Hoare triple \{$S\wedge B$\} $P$ \{$S$\} holds, then the
following Hoare triple will hold:
\end{thm*}
\begin{lyxcode}
\{$S$\}

while~condition~$B$~do

~~$P$

end\_while

\{$S\wedge B'$\}
\end{lyxcode}

\subsection{A simple example}

Consider this little program:

\begin{lyxcode}
Product(x,y)

//~Precondition:~x~and~y~are~non-negative~integers

//~Postcondition:~returns~the~product~of~x~and~y

begin~

~~i:=0;

~~j:=0;

~~while~(~(i=x)'~)~do

~~~~j=j+y;

~~~~i:=i+1;

~~end~while

~~//~Assertion:~\{~j~=~x{*}y~\}

~~return(j);

end;
\end{lyxcode}
It's pretty clear that this algorithm it's correct.

Let's check it anyway to see how it works.

\begin{proof}
We need a loop invariant, which will describe the state of the program
after $k$ iterations. 

A reasonable guess is $S$ : $j=iy$

Let $i_{k}$, $j_{k}$ and $S_{k}$ be the value of $i$, $j$ and
$S$ after $k$ iterations.

Base case: using the assignment rule, $i_{0}=0$ and $j_{0}=0$ so
$S_{0}$ holds.

Induction step:

Assume the invariant holds after $k-1$ iterations: $j_{k-1}=i_{k-1}y$

We need to prove that the invariant is preserved by the $k$ th iteration.

Otherwise said, we have to check that the following Hoare triple holds:
\begin{lyxcode}
\{$S_{k-1}\wedge(i=x)'$\}

~$j_{k}:=j_{k-1}+y$;

~$i_{k}:=i_{k-1}+1$;

\{$S_{k}$\}
\end{lyxcode}
Let's applying the assignment rule. 

By substituting $i_{k}$ and $j_{k}$ by the expressions they have
been assigned with, we get:

\[
\begin{array}{rclcll}
S_{k} & \Leftrightarrow & j_{k} & = & i_{k}y & \textrm{ }\\
\textrm{ } & \Leftrightarrow & j_{k-1}+y & = & (i_{k-1}+1)y & \textrm{ }(\textrm{By the substitution rule})\\
\textrm{ } & \Leftrightarrow & i_{k-1}y+y & = & (i_{k-1}+1)y & \textrm{ }(\textrm{By }S_{k-1})\\
\textrm{ } & \Leftrightarrow & i_{k-1}y+y & = & i_{k-1}y+y\end{array}\]


So, $S_{k}$ indeed holds.

By induction, after any number $k$ of iterations, $S_{k}$ still
hold.

At the end, both $S_{k}$ and $i=x$ hold, so, as expected: $j=iy=xy$
\end{proof}
\begin{rem*}
We have proved that after the end of the execution the result is correct.

But what if the program does not terminate and loop forever?

This is not usually consider a proper behavior.

We only have spoken about \emph{partial-correctness.} 

A full proof of correctness needs also a proof of termination!
\end{rem*}

\subsection{A more sophisticated example: The Euclidean algorithm}

\begin{lyxcode}
GCD(a,b)

Begin

//~Precondition:~a~and~b~are~non-negative~integers~~

//~with~a>=b.

//~Postcondition:

//~returns~gcd(a,b),~the~greater~common~divisor~of~

//~a~and~b.

Local~variables:~i,~j,~q,~r

~~i:=a;

~~j:=b;

~~while~j>0~do

~~~~//~Assertion:~

~~~~//~r~is~the~rest~of~the~integer~division~i/j

~~~~r:=~i~mod~j;

~~~~i:=~j;

~~~~j:=~r;

~~end~while

~~//~Assertion:~i~is~the~gcd~of~a~and~b.

~~return(i);

end;
\end{lyxcode}
\begin{xca}
Use the Euclidean algorithm to compute:

\texttt{GCD(8,8)}, \texttt{GCD(14,4)}, \texttt{GCD(31,17)}.
\end{xca}
Here the proof of correctness of the algorithm is non-trivial.

\begin{proof}
Let $i_{k}$ and $j_{k}$ be the value of $i$ and $j$ after $k$
iterations.

We need to find an invariant which describes the state of the program
after each iteration.

Take $S_{k}$: $\textrm{gcd}(i_{k},\textrm{ }j_{k})=\textrm{gcd}(a,b)$.
\begin{enumerate}
\item Base case:


Before the loop, $i_{0}=a$ and $j_{0}=b$.

So the invariant $S_{0}$ holds: $\textrm{gcd}(i_{0},\textrm{ }j_{0})=\textrm{gcd}(a,b)$;

\item Induction step:


Assume $S_{k-1}$ holds, that is $\textrm{gcd}(i_{k-1},\textrm{ }j_{k-1})=\textrm{gcd}(a,b)$.

We just need to prove that $\textrm{gcd}(i_{k},\textrm{ }j_{k})=\textrm{gcd}(i_{k-1},\textrm{ }j_{k-1})$.

By the assignment rule, we have:

\begin{itemize}
\item $r$ is the rest of the division of $i_{k-1}$ by $j_{k-1}$,
\item $i_{k}=j_{k-1}$,
\item $j_{k}=r$. 
\end{itemize}
So, by the definition of the integer division, we have:

\[
i_{k-1}=qj_{k-1}+j_{k}\]
 for some integer $q$.

\begin{enumerate}
\item Assume $x$ divides both $i_{k}$ and $j_{k}$.


Then, of course $j_{k-1}$, since $j_{k-1}=i_{k}$.

By the equation above, $x$ also divides $i_{k-1}$.

\item Assume $x$ divides both $i_{k-1}$ and $j_{k-1}$.


Then of course $x$ divides $i_{k}$.

Once again, using the equation above, $x$ also divides $j_{k}$

\end{enumerate}
Therefore, $\textrm{gcd}(i_{k},\textrm{ }j_{k})=\textrm{gcd}(i_{k-1},\textrm{ }j_{k-1})=\textrm{gcd}(a,b)$,
as wanted.

\item At the end:


By induction, the loop invariant $S$ still holds: $\textrm{gcd}(i,\textrm{ }j)=\textrm{gcd}(a,b)$

Moreover, the loop condition failed: $j=0$.

So, $\textrm{gcd}(a,b)=\textrm{gcd}(i,\textrm{ }j)=\textrm{gcd}(i,\textrm{ }0)=i$,
as expected.

\end{enumerate}
\end{proof}

\section{Conclusion}


\subsection{A note on automatic program proving:}

\begin{itemize}
\item There is no mechanical way to decide even if a program terminates
or not.
\item Traditional imperative languages:

\begin{itemize}
\item Automatic proving is very difficult because of \emph{side effects}
\item side effects needs to be considered as some form of output
\end{itemize}
\item Functional languages (lisp, scheme, ML, caml):

\begin{itemize}
\item Designed to make it easier to prove correctness
\item Fun to program. Try them!
\end{itemize}
\item Two difficulties: 

\begin{itemize}
\item Finding the correct assertions
\item Checking that the implications holds
\end{itemize}
\item Mixed approach:

\begin{itemize}
\item The programmer gives the main assertions
\item The prover derives the other assertions
\end{itemize}
\end{itemize}

\subsection{Check assertions in your programs!}

\begin{itemize}
\item Use static type checking / assert / exceptions
\item When debugging, you can ask for all assertions to be checked
\item Documentation
\item Help for the proof
\end{itemize}

\end{document}
