\documentclass[12pt]{amsart}
\usepackage{boxedminipage}
\input{defalgo.tex}
\usepackage{program}
\usepackage{epsf}
\input{defcode}

\title{An Introduction to Program Correctness and Complexity\\
\emph{(draft notes)}}

\author{Raul H.C. Lopes}

\begin{document}
\nocite{broy:cmcs}
\maketitle
\section{Algorithms}


Algorithms have been frequently characterized as finite descriptions of computations that should always be effective (mechanically executable), terminating
(the algorithm comes to an end after a finite time for any input), and deterministic (the course of execution is uniquely defined for a given input.) (See
initial chapters of \cite{bauer:alpd} and \cite{rogers:rf} for considerations
on the concept of algorithm.)

Experience with randomized algorithms (see \cite{motwani:randomized}) and 
with non-determinism as a tool for specification of concurrent and sequential
algorithms \cite{dijkstra:discipline} suggests incorporating non-determinism,
parallelism, and non-termination as admissible characteristics of algorithms
(Knuth (in \cite{dek:taocp:i}) prefers the name \emph{computational method}
when non-termination and non-determinism are admitted.)


\subsection{Algorithm characterization}

An algorithm can always be characterized with respect to, at least, the following aspects:
\begin{itemize}
\item\textbf{Finiteness of description:} every algorithm should have a finite
textual representation
\item\textbf{Effectiveness:}  each one of its step should be mechanically executable.
\item\textbf{Termination:} Does the algorithm come to an end after a finite number of \emph{transitions}?
\item\textbf{Determination:} is the course of execution for a given input
uniquely defined?
\item\textbf{Efficiency:} How many resources (memory, transitions/time) does
the algorithm demand?
\end{itemize}
 
\subsection{Non-determinism and concurrency}

\subsubsection{Pre-algorithmic formulation}

Bauer and W\"ossner \cite{bauer:alpd} introduce the idea of using \emph{pre-algorithmic} construction in the first stages of problem specification.

\begin{bxalgorithm}\label{gcdchoice}
\begin{program}
\FUNC gcd(a\in\NAT  b\in\NAT)\map \NAT \equiv
\precond{a\neq 0\pcor b\neq 0}
\ \tab \xquant{\some}{t}{t\in\NAT}{t\mid a \pcand t\mid b \pcand \xquant{\forall}{y}{y\in\NAT}{y\mid a \pcand y\mid b \pcimp y\leq t}}
\end{program}
\end{bxalgorithm}

Definition above states that \emph{gcd} is a function 
that  when given two arguments in $\NAT$ (intuitively the set of natural numbers),
with the pre-condition that at least one of them is not zero, produces some
number $t$ such that:
\begin{itemize}
\item $t\in \NAT$
\item $t$ divides (symbol $\mid$) both $a$ and $b$;
\item for any $y\in\NAT$ that divides $a$ and $b$, $y\le t$.
\end{itemize}

$\some$ is a choice operator: a non-deterministic one that chooses any element
from a given set. Gurevich in his \emph{Abstract State Machines} (\cite{gurevich:lipari}) also defines a choice operator.

The \emph{function} in \ref{gcdchoice} does not state a finite sequence of
steps to find the greatest common divisor. It is, however, useful as 
a first definition of what must be produced. Bauer and W\"ossner refine
this definition to \ref{gcdtheone}, where the operator $\theone$ is used
in the sense of selecting the unique element of a given set that satisfies
some property. Should there be more one element satisfying the property
and the computation would \emph{diverge}, for example, finishing with 
undefined ($\diverge$) result. 

\begin{bxalgorithm}
\label{gcdtheone}
\begin{program}
\FUNC gcd(a\in\NAT  b\in\NAT)\map \NAT \equiv
\precond{a\neq 0 \pcor b\neq 0}
\ \tab \xquant{\theone}{t}{t\in\NAT}{t\mid a \pcand t\mid b \pcand \xquant{\forall}{y}{y\in\NAT}{y\mid a \pcand y\mid b \pcimp y\leq t}}

\end{program}
\end{bxalgorithm}

\begin{exercise}
Prove that \ref{gcdtheone} does not diverge.
\end{exercise}

\subsubsection{Logical description}

A program to evaluate the maximum of a given set of numbers could be initially
described as the function in \ref{maxchoice}.
\begin{bxalgorithm}
\label{maxchoice}
\begin{program}
\FUNC max(S\subset\NAT)\map\NAT\equiv
\ \tab\xquant{\some}{x}{x\in S}{\xquant{\forall}{y}{y\in S}{y\le x}}
\end{program}
\end{bxalgorithm}

\emph{Fact:} An execution of a program can be represented as the sequence 
of states.

\begin{itemize}
\item\textbf{state}: a state of a program is an assignment of values to all its 
variables.
\item\textbf{action:} a temporal logic expression, defining a relation between
\emph{old states} and \emph{new} states. For example,

\[\CO{p}{q}\]

that states (using Hoare triples)

\[\forall \alpha. \hoare{p}{\alpha}{q}\]

if $p$ is true of a given state, after any action of the system in that state,
$q$ will hold in the resulting state.

An action is a logical relation constraining the \emph{transitions}, or 
\emph{updates} in the language of \cite{gurevich:lipari}.
 (I'll use the terms 
\emph{transition} and \emph{update} to designate synonyms for the 
usual \emph{step} of a program, and say that actions constraining the 
transitions/steps of a program.)
\end{itemize}

A logical description of a program defines a set of conditions that any
implementation of it should satisfy. 
Misra,
in \cite{misra:unity88,misra:unity94}, 
uses a formal system (called UNITY), which combines a temporal logic 
to present   logical descriptions of programs and a language (whose
semantics is expressed in the logic of UNITY) for representing operational
descriptions of programs. As an example, he introduces a program for computing
the maximum of a set of numbers as is given in \ref{maxlogical}. Notice
the use of the 
operator {\bf co} described above. 

\begin{bxalgorithm}
\label{maxlogical}
\begin{program}
\PROG max
\initially\ v=-\infty
\alpha: \CO{v=m}{v=m \pcor (v\in S \pcand v>m)}
\beta: m\in S \leadsto v\ge m
\end{program}
\end{bxalgorithm}

In a logical description, the steps to be performed are described through
predicates
that represent logical relation between states.
In a sense, \ref{maxlogical} above describes
a family of programs. The programs in that family should obey the following
conditions:
\begin{itemize}
\item $\initially\ v=-\infty$

Before any computation $v$ must be initialized to $\infty$.

\item $\CO{v=m}{v=m \pcor (v\in S \pcand v>m)}$

which states that $\forall m.\forall\alpha:\hoare{v=m}{\alpha}{v=m\pcor(v\in S \pcand v>m)}$

For any \emph{transition} in this program, if $v$ equals $m$ before the transition, then after it either $v$ is still equal to $m$ or it has been changed to some
value from $S$ and $v>m$.

\item $m\in S \leadsto v\ge m$

that establishes that for any $m$ if $m\in S$ in a given state,
 then eventually $v$ will be greater
or equal than $m$.

\end{itemize}


\subsubsection{States and transitions}
\begin{itemize}
\item\textbf{state:} a snapshot of a given execution: the assignments of values
to variables;
\item\textbf{action:} a logical relation between states; it restricts the 
possible transitions from a state.
\item\textbf{behaviour (run or execution:} a sequence of state $\seq{s_0,s_1,s_2,ldots}$, such that $s_0$ is produced by the initialization of the program
and each $s_{i+1}$ is obtained from $s_i$ by some transition of the
given program. 
\item\textbf{stable property:} a property whose truth is not affected by any 
transition: if it holds before; it still holds after the transition.
\item\textbf{invariant property:} a property the holds after initialization
and is stable.
\item\textbf{safety conditions:} expressed through invariant properties they 
establish that the transitions are safe, in Lamport's words, \emph{bad
things don't happen.}
\item\textbf{progress conditions:} they state the program/system is on
the move.
\end{itemize}

\subsubsection{Proving program properties}
Given a program, maybe through a logical description, one is usually interested
in investigating at least the following properties of that program:
\begin{itemize}
\item \emph{safety} of the results: does it always compute the expected output?
\item \emph{termination} of computation: does the computation ever reach a
halting state, when no variables are changed and nothing useful is computed?
\item\emph{complexity} of computation: how long does it take to reach the 
halting state?
\end{itemize}

The following definition will be used in the study of program properties.
\begin{definition}
\ \\
\begin{itemize}
\item $\stable{p} \equiv \CO{p}{p}$

A property is stable when its truth is not changed by any transition: if $p$
is true in a state, it will still be true after any transition from that 
state.


\item $\invariant{p} \equiv \initially{p} \pcand \stable p$

A property about a program is invariant if it is true after initialization and
is kept true for any execution of the program.
\end{itemize} 
\end{definition}

\begin{notation}
The notation of \cite{dijkstra:fpd} will be followed and curried notation will
be used for function
application, using
\[ f.i.j \]
to denote the aplication of $f$ to $i$ and $j$.
As usual, an application to a tuple of values is acceptable as in
\[  max(x,y)\]
A sequence of $\tau$ is understood as a mapping from integers to $\tau$, and
in principle an array will be seen a function.


\end{notation}



We can prove about \ref{maxlogical} that
\[ \stable{v\le max.S} \]

where \[max.S=\xquant{\some}{x}{x\in S}{\xquant{\forall}{y}{y\in S}{y\le x}}\]

\begin{Proof}
\begin{enumerate}
\item $\forall m:\CO{v=m}{v=m \pcor (v\in S \pcand v>m)}$

\proofjust{{\rm\bf from\ }\alpha}

\item $\CO{v=m_0}{v=m_0\pcor (v\in S \pcand v>m_0)}$

\proofjust{\alpha{\rm\ for\ }m=m_0\rangle}

\item $m_0 \le max.S$

\proofjust{{\rm\bf stability\ of\ } v\le max.S}
 
\begin{enumerate}
\item either $v=m_0$, and as such $v\le max.S$

\proofjust{\mathrm{\bf first\ outcome\ of\ } \alpha}
\item or $(v\in S \pcand v>m)$, and $v\le max.S$ by the first conjunct.

\end{enumerate}

\end{enumerate}
%\begin{flushright}
%$\Box$
%\end{flushright}
\end{Proof}

It can also be proved about the program \ref{maxlogical} that \emph{eventually}
$v\ge max.S$ also written as 
\begin{itemize}
\item $\eventually v\ge max.S$
\item $true \leadsto v\ge max.S$

\end{itemize}

\begin{Proof}
\begin{enumerate}
\item $m\in S\leadsto v\ge m$
\proofjust{{\rm\bf from\ } \beta}

\item $max.S\in S\leadsto v\ge max.S$
\proofjust{\mathrm{\mbox{\bf for }}m=max.S}
\item $true \leadsto v\ge max.S$

\proofjust{\mathrm{\mbox{\bf from the truth of } max.S\in S}}
\end{enumerate}

\end{Proof}

Misra, in \cite{misra:unity94}, presents formal derivations for the properties
above.

\subsubsection{Operational description}


A possible refinement, still in UNITY and presented in \cite{misra:unity88}, of \ref{maxlogical} follows in \ref{maxassync}.


\begin{bxalgorithm}
\label{maxassync}
\begin{program}
\PROG assyncmax

\declare v,i\in\NAT
\initially v:=-\infty;
\assign
\ \ \tab \xquant{\assync}{i}{0\le i<\szof{S}}{v=:max(v,S.i}
\end{program}
\end{bxalgorithm}
Notice the use of \emph{max} as a binary operator:  it is supposed to
yield  the maximum of its two arguments.

\begin{notation}
\[\szof{S}\]
will be used to denote the number of elements of $S$, when $S$ is either a
set or a sequence.
\end{notation}

In UNITY, the statements in an \emph{assign-section} are separated by the
symbol {\assync}, that indicates an assynchronous execution of the statements
in the section, each one being atomic. In this draft, strong fairness is
assumed. For example, it is assumed that the  program \ref{maxassync} executes
\[v=max(v,S.0), v=max(v,S.1), v=max(v,S.2), \]
forever an in a non-specific order, with each $v=max(v,S.i)$ being chosen (executed) infinitely often.

\begin{itemize}
\item this a non-deterministic formulation;
\item essentially parallel;
\item eventually some $i$, such that $S.i=max.S$, will
be chosen and $v$ will be equal to $max.S$.
\end{itemize}

\subsection{Fixpoints}

\begin{definition}
\textbf{Fixpoint} {\DEF} a state of the computation where no further work produces any change in the program's variables. 
\end{definition}

Program \ref{maxassync} reaches a fixpoint when $m=max.S$.
\begin{Proof}
\begin{enumerate}
\item $\fp{}\equiv\xquant{\forall}{i}{0\le i<\szof{S}}{v=max(v,S.i)}$

The fixpoint is reached when $v$ doesn't change, and that means $v$ is
$max(v,S.i$ for any $i$.
\item $\fp{}\equiv\xquant{\forall}{i}{0\le i<\szof{S}}{v\ge S.i}$
\item $\fp{}\equiv v\ge\xquant{max}{i}{0\le i<\szof{S}}{S.i}$


\end{enumerate}

\end{Proof}

\section{Examples}
A set of examples dealing with: invariant properties, loop guards, bound 
functions, algorithmic complexity.

\subsection{Maximum again}
A further, deterministic, refiniment for that program follows in \ref{maxsync}.

\begin{bxalgorithm}
\label{maxsync}
\begin{program}
\PROG maximum
\declare v,i\in\NAT
\initially v,i:=-\infty,0;
\assign
\ \tab i<\szof{S}\map v,i:=max(v,S.i),i+1; 
\end{program}

\end{bxalgorithm}

\subsubsection{Fixpoint}

\begin{itemize}
\item $v,i:=max(v,S.i),i+1$ is the equivalent of
\begin{program}
\psync v:=max(v,S.i)
\psync i:=i+1
\end{program}
and that means the statements are executed in parallel and they should be
treated as atomic.
\item $\fp{}\equiv i\ge \szof{S}$
\item $i$ is incremented in each transition: thus, eventually $i\ge \szof{S}$

\end{itemize}

\subsubsection{Bound function}
\begin{itemize}
\item |maximum| can be seen as scanning the sequence |S| from left to right. 
\item A \emph{bound function} (also called \emph{derived variable}) can be defined to
establish that  \emph{work} must still be performed.
It is a  function of the variables of the program. 
It is introduced to define a limit on the transitions that must still
be performed: when such limit is reached, no other transition will produce
useful changes in the program's variables. 
\item let $t$ (the bound function) be $\szof{S}-i$.
\item It can easily be checked that
\begin{enumerate}
\item assuming that $t'$ is value of $t$ after a transition, it can be proved that,
for any transition, either $t>t'$ or $t=t' \pcand t=0$ (when no transition is performed that changes the programs variables: after $t=0$, $t$ doesn't change anymore.)

\begin{notation}
Given a transition $\alpha$ and a variable $x$ that can (possibly) be changed by $\alpha$, $x'$ will be used to denote the value of $x$ after $\alpha$.
\end{notation}

\begin{Proof}
\begin{alignat*}{3}
 t &=\szof{S}-i & \text{ definition of } t  \\
 t' &=\szof{S}-i' & \\
 i' &=i+1 & \text{ program inspection} \\
 t' &=\szof{S}-(i+1) & \\
    &=\szof{S}-i-1 & \\
    &=t-1 &  
\end{alignat*}
\end{Proof}

\item  when $i=\szof{S}$, $t=0$.
\item $t$ gives at any moment the size of task ahead: in this problem, it
gives exactly the number of transitions
to be performed.
\item initially the number of tansitions to be performed is $\szof{S}$.
\end{enumerate}


\end{itemize}

\subsubsection{Complexity}

|maximum| always performs $\szof{S}$ transitions when given a set |S|.
Its complexity is said to be 
$O(\szof{S})$.

\begin{definition}
$g(n) = O(f(n))$ means that there are constants $k$ and $n_0$ such that for 
all $n>n_0$ \[g(n) \le k f(n)\]
\end{definition}

\subsubsection{Invariant property}
\begin{itemize}
\item $P\DEF (0\le i\le\szof{S})\pcand (v=\xquant{max}{k}{0\le k<i}{S.k})$
\item \stable{P}
\begin{Proof}
Assuming $P$ is true before a transition, there are two cases:
\begin{enumerate}
\item $i=\szof{S}$, before the transition: the variables don't change and
$P$ remains true (fixpoint case.)
\item $i< \szof{S}$ before the transition
\begin{alignat*}{3}
 &i'=i+1 & \\
 &i'-1=i<\szof{S} &\\
 &i'<\szof{S}+1  & \\
 &i'\le\szof(S) & ;P' \textbf{: 1st conjunct} \\
 &v'=max(v,S.i) & \\
 &v'=max(\xquant{max}{k}{0\le k<i}{S.k}),S.i) & ;\text{ from } P \\
 &v'=\xquant{max}{k}{0\le k\le i}{S.k} & ; P' \text{: 2nd conjunct} 
\end{alignat*}



\end{enumerate}


\end{Proof}
 
\item \invariant{P}: from \stable{P} and from the truth (trivially checked)
of $P$ after initialization.

\item When fixpoint is reached, $P$ holds, and consequently $v$ holds
the maximum of all $S.i$.

\end{itemize}

\subsection{A multiplication algorithm}

\begin{bxalgorithm}
\label{peasant}
\begin{program}
\PROG mult
\precond{A,B \in \NAT}
\poscond{z=A*B}
\declare x,y,z \in \NAT;
\initially x,y,z:=A,B,0;
\assign y>0 \uthen \tab \assync even(y) \uthen x,y:=2*x,y/2
			\assync odd(y) \uthen y,z:=y-1,z+x 
\end{program}

\end{bxalgorithm}


\begin{itemize}
\item let $P\DEF x*y+z=A*B $
\item $\initially\ P$

Because initially $x=A,y=B,z=0$.

\item \stable{P}

\begin{Proof}
Assuming that $P$ holds before the transition.

\begin{itemize}
\item $y=0$ then there are no changes in variables and $P$ holds after the transition.
\item $y>0$ then $P'\equiv x'*y'+z'=A*B$

\begin{alignat*}{2}
\mathrm{\mbox{\bf when $y$ is odd:: }}& x'=x,y'=y-1,z'=z+x &  \\
x'*y'+z' &= x*(y-1)+(z+x)  \\
 &= xy-x+z+x  \\
 &= x*y+z  \\
 &= A*B  \mathrm{\mbox{ ; because $P$ holds before}}\\
 & \\
\mathrm{\mbox{\bf when $y$ is even: }}& x'=2*x,y'=y/2,z'=z \\
x'*y'+z'& = (2*x)*(y/2)+z  \\
 &= xy+z \\
 &= A*B  \mathrm{\mbox{ ; because $P$ holds before}}
\end{alignat*}

Thus $P$ holds after the transition.
\end{itemize}
\end{Proof}

\item \invariant{P}

Because $\initially P$ and \stable{P}.

\end{itemize}

\subsubsection{A fixpoint}
The algorithm eventually reaches a fixpoint.
\begin{Proof}
\begin{itemize}
\item $\initially y\ge 0$ because $B\in\NAT$ 
\item every transition (while $y>0$) either decrements $y$ by $1$ or divides
$y$ by $2$
\item Thus, eventually, $y$ becomes $0$ and no other changes are made in the
program's variables.
\end{itemize}

\end{Proof}

When the fixpoint is reached $y=0$ and the equality $x*y+z=A*B$ establishes
\[z=A*B\]

\subsection{The complexity}
The algorithm takes $O(\lg B)$ transitions to reach a fixpoint.
\begin{itemize}
\item We  assume B is a power of 2 and define
\begin{align}
T(0)&=0 \mathrm{\mbox{; when $y=0$ the fixpoint has been reached}}\\
T(1)&=1 \\
T(2^k)&=1+T(2^{k-1})\mathrm{\mbox{; for $k> 0$ each transition divides $y$ by 2}}\label{recurrence}
\end{align}

\item $T(y)$ counts the number of transitions that must be performed to reach 
a fixpoint, for a given $y$. Given a $y>0$ the number of transitions to be 
be performed is $1$ (the one that divides $y$ by $2$) plus the number
of transitions necessary for $y/2$ (given by $T(y/2)$.) 

\item $T(y)$ above is a \emph{recurrence relation} and it is not hard to see 
and prove that $(1+\lg y)$ is a solution for that relation.

\item Equation \ref{recurrence} above can be solved by a method called iterationwhich consists in recurrently replacing the right-hand side occurrence of
$T$ by its definition:
\begin{align*}
T(2^k) &= 1+T(2^{k-1}) \\
 &= 1+(1+T(2^{k-2})) \\
 &= 1+(1+(1+T(2^{k-3}))) \\
 &= \underbrace{1+1+\ldots+1}_{k}+T(1) \\
 &= k+1
\end{align*} 

\item That $T(n)=(1+\lg n)$ is proved by induction:
\begin{Proof}
\begin{align*}
\mathrm{\mbox{\bf when n=1: }} (1+\lg{n})=1=T(1) &\\
\mathrm{\mbox{\bf assuming it true for $n<2^k$\ }} &\\
\mathrm{\mbox{\bf for $n=2^k$:}}\qquad 
T(2^k)&=1+T(2^k)\\
     &= 1+(1+\lg{2^{k-1}}\\
     &= 1+k
\end{align*}
\end{Proof}

\item when $y$ is odd, we add to the recurrence relation
\[T(2*n+1)=1+T(2*n) \mathrm{\mbox{, when $y$ is odd}}\]

\item It can be proved by induction that if there is $m$ such that 
\[2^m < (2n+1) < 2^{m+1}\]
then
\[T(2n+1)< T(2^{m+1})\]

\item From that, we conclude that $T(n)=O(\lg n).$

\end{itemize}

\begin{exercise}
Prove that $T(n)=O(\lg n)$ when $T(n)$ is defined as above.
\end{exercise}

\begin{note}
Program \ref{peasant} is adapted from \cite{gries:science-prog}.
\end{note}

\subsection{Linear search}
Given: a sequence $S$ with $n$ integers and an integer $x$.
%, known to be
%in the sequence. 
We are asked to find the first occurrence of $x$ in the
sequence.
\begin{bxalgorithm}
\label{linsearch}
\begin{program}
\PROG linearSearch
\precond{S \in \{0\ldots n-1\}\map \INT, x\in\INT, x\in S}
\poscond{(i=n\pcand x\not\in S)\pcor(0\le i<n \pcand x=S.i)}
\declare i \in \NAT;
\initially i:=0;
\assign i<n \uthen \tab \assync x\neq S.i \uthen i:=i+1
		        \assync x=S.i \uthen skip
\end{program}


\end{bxalgorithm}

\begin{notation}
$skip$ does nothing.
\end{notation}

\subsubsection{Invariant}
Define 
\[ P\DEF (0\le i\le n)\pcand(\xquant{\forall}{k}{0\le k<i}{x\neq S.k}\]

\begin{exercise}
Prove 
\[\invariant{P}\]
\end{exercise}

\subsubsection{Fixpoint}

The program reaches a fixpoint when $i=n$ or $x=S.i$.

\subsubsection{Complexity}
Assuming $x$ occurs in $S$.

\begin{itemize}
\item\textbf{Best case:} $x$ is in $S$ and is the first item: one comparison
is made and the time spent O(1).
\item\textbf{Worst case:} $x=S.(n-1)$ and $n$ transitions (comparisons)
are performed
until the firxpoint is reached.
\item\textbf{Average case:} 
\begin{enumerate}
\item assign probability $p_i$ to kind of problem
\item $\sum_{1\le i\le n}p_i=1$
\item $T_{\rm average}=\sum_i p_{i}T_i$
\item In this case, there are $n$ problems: the possible occurrences of
$x$ in $S$
\item $p_i=1/n$
\item \[T = \sum_{1\le i\le n} i/p_{i}=\frac{n+1}{2}\]
\end{enumerate}

\end{itemize}

\begin{exercise}
What if we had not assumed that $x$ occurs in $S$?
\end{exercise}

\begin{note}
Program \ref{linsearch} is adapted from \cite{gries:science-prog}. The
analysis of its complexity is presented in \cite{purdom:analysis}.
\end{note}

\begin{exercise}
Write a program that, given a sequence $S.(0..n-1)$, will set the following
output condition:
\[ x\le S.(0..n-1) \pcand \xquant{\exists}{j}{0\le j< n}{x=S.j}\]
\begin{enumerate}
\item Describe your invariant, and bound function.
\item Prove correctness.
\item Consider at least two alternatives (i.e., different programs) 
representing different search strategies over your sequence.
\end{enumerate}

\textbf{(Adapted from \cite{gries:science-prog}.)}

\end{exercise}


\subsection{Bidimensional search}
Given a two-dimensional sequence of integers $S.(0..m-1)..(0..n-1)$, and 
an integer $x$, find out whether $x$ is in $S$.

In the figure that follows the box represents the sequence to be searched,
and the shaded area, an area that has already been scanned and that is
known not to contain $x$.

$$\epsfbox{bidimen.1}$$

The work to be done is to search the whole sequence until $x$ is found.
Assume that $i$ and $j$ are used to index the sequence, the target
output becomes:
\[ R \DEF (i=m \pcand x\not\in S) \pcor (0\le i< m \pcand 0\le j<n \pcand x=S.i.j) \]

From the figure above, an invariant becomes evident: while the search proceeds
\emph{x is not the shaded area.}
\begin{align*}
 P \DEF 0\le &i\le m\pcand 0\le  j<n \\ &\pcand x\not\in S.(0..i-1).(0..m-1)\\
 &\pcand x\not\in S.i.(0..j-1)
\end{align*}

$P$ expresses the assurance that $x$ has not been found before $S.i.j$,
which is at any moment the only reason to proceed with the search.

That defines a safety condition. However, that's not enough: progress must be
made and that means extending the shaded area. The unshaded area represents
the work to be done:
\[ w=(m-i)*n-j \]

Progress is obtained if each step enforces 
\[ w > w' \]
and that means increasing either $i$ or $j$. But, increasing $i$ or $j$ means
bringing more area into the shaded part of the box, the one that's considered
as already scanned and not containing $x$. Thus,

\textbf{Restriction:} $w$ can be decreased (and the shaded area extended) only 
if $x$ has not been found: $x\neq S.i.j$.

In addition, there must be assurances that the search will go beyond the
limits of $S$:

\textbf{Restricton:} proceed at most until the whole area is shaded: $w=0$.

A first refinment of our program follows:

\begin{bxalgorithm}
\label{twodsearch}
\begin{program}
\PROG bidimen
\initially
\ \ i,j:=0,0;
\assign 
\ \ (m-i)*n-j>0 \pccand x\neq S.i.j\AR \text{\mbox{"increase either $i$ or $j$"}}
\end{program}
\end{bxalgorithm}

Increasing either $i$ or $j$ decreases the unscanned area, but that must be
orderly, expressing the idea of testing each element of the sequence.
Following
the figure, $j$ will be increased until $n$ while $i$ is kept fixed and
(when $j$ reaches $n$) $i$ will be increased to start a new line. 
Finally, when $i$ gets to $m$ $w$ equals to $0$: the condition $w>0$
can be simplified to $i<m$.
Program
\ref{twodsearch} is now refined to:

\begin{bxalgorithm}
\label{bidsearch}
\begin{program}
\PROG bidimen
\initially
\ \ i,j:=0,0;
\assign 
\ \ i<m \pccand x\neq S.i.j\AR i,j:=\tab i,j+1,\ if\ j<n
                                         i+1,0,\ if\ j=n 
\end{program}
\end{bxalgorithm}

\begin{exercise}
Prove that:
\begin{enumerate}
\item That $P$ is and invariant for program \ref{bidsearch}
\item That $w>w'$ is also an invariant for that program.
\item Program \ref{bidsearch} has a fixed point.
\end{enumerate}

\end{exercise}

Program \ref{bidsearch} is developed by Gries in \cite{gries:science-prog}
where he develops the loop guard
\[ B \DEF i\neq m \pccand S.i.j \]

by observing that $B$ such that when a fixpoint is reached ($\neg B$ is true)
$P$ and $R$ must be true. In other words:
\[ P \pcand \neg B \pcimp R \]

\begin{exercise}
Write a program to find the greatest common divisor for two given integers
$X>0$ and $Y>0$.
\begin{enumerate}
\item Use only additions and subtractions.
\item Prove correctness.
\begin{itemize}
\item Use invariant
 \[ x>0 \pcand y>0 \pcand gcd(x,y)=gcd(X,Y) \]
where $x$ and $y$ are initialized to $X$ and $Y$.
\item use bound function $w=x+y$. (This time the bound function won't provide
the complexity for your algorithm. It will just give  the limit when a fixpoint 
is reached.)
\item Build your program to ensure that $x>0$ and $y>0$ are always true and
use that to prove termination.
\end{itemize}
\end{enumerate}

\end{exercise}


\subsection{Bentley's split}
Given is a sequence $S.(0..n-1)$ of integers, and the index $p$ of one of them, called \emph{splitter}. 

\textbf{Target:} partition the sequence in 3 subsequences respectivelly composed of
the elements less than the splitter, those equal to it, and  those greater
than it.

An algoritm is presented in \cite{bs:ternary} which consists of 
2 steps:
\begin{enumerate}
\item partition the sequence in 4 subsequences, as shown in the figure below:
$$\epsfbox{bentley.split.1}$$

\item move the 2 subsequences containing elements equal to the splitter to
the center, as shown in the figure below:

$$\epsfbox{bentley.split.2}$$


\end{enumerate}

\subsubsection{Partitioning into 4 subsequences}
Four pointers will be defined to marked the limits of the patitions being 
constructed:
\begin{itemize}
\item\textbf{nel}: the insertion point for the next element equal to the splitter
on the left side;
\item\textbf{lt}: the next insertion point for elements less than the spilter;
\item\textbf{ner}: the insertion point for the next element equal to the splitter
on the right side;
\item\textbf{gt}: the next insertion point for elements greater than the spilter;

\end{itemize}
The process should start with the pointers marking 4 empty partitions 
($nel=lt=0, ner=gt=n-1$), as illustrated below:

Assuming that $S_0.(0..n-1)$ denotes the initial subsequence, the desired 
output is given by
\begin{align*}
 & S \text{\mbox{ is a permutation of }} S_0 \\
 \pcand & \xquant{\forall}{j}{0\le j<nel}{S.j=S_0.p}\\
 \pcand & \xquant{\forall}{j}{nel\le j<lt}{S.j<S_0.p}\\
 \pcand & \xquant{\forall}{j}{gt<j\le ner}{S.j>S_0.p}\\
 \pcand & \xquant{\forall}{j}{ner<j\le 0}{S.j=S_0.p}\\
 \pcand & gt<lt
\end{align*}

\begin{exercise}
Define a logical expression for 
\[S \text{\mbox{ is a permutation of }} S_0 \]
\end{exercise}

The four partitions must be initially empty and located at the extremes of
the array, corresponding to the following initialization:

\begin{align*}
 lt=nel=& 0  \\
 gt=ner=&n-1
\end{align*}

Progress will be achieved by incorporating new elements to any of four
partitions being built. At any time, $lt$ will point the first non-incorporated
element from the left; $gt$ will point the first non-incorporated element
from the right. Each incorporation of some element to one of the four partitions
should keep the following true:

\begin{align*}
 P \DEF&
  S \text{\mbox{ is a permutation of }} S_0 \\
 \pcand & \xquant{\forall}{j}{0\le j<nel}{S.j=S_0.p}\\
 \pcand & \xquant{\forall}{j}{nel\le j<lt}{S.j<S_0.p}\\
 \pcand & \xquant{\forall}{j}{gt<j\le ner}{S.j>S_0.p}\\
 \pcand & \xquant{\forall}{j}{ner<j\le n-1}{S.j=S_0.p}\\
 \pcand & \xquant{\forall}{j}{lt\le j\le gt}{S.j=S_0.j}
\end{align*}

A \emph{limit on the progress} will be defined by observing that elements
are incorporated from the left by increasing $lt$ and from the right by
decreasing $gt$. As soon as they cross each other, the process should be
stopped: all elements having been incorporated into one of the partitions.

The following conditions are thus defined:
\begin{itemize}
\item\textbf{bounds for the pointers}
\begin{align*}
 B_0 \DEF & 0\le nel\le lt \\
 B_1 \DEF & gt\le ner < n \\
\end{align*}
\item partition \textbf{safety} is guaranteed by $P$
\item\textbf{bound function:}
\[ w\DEF gt-lt+1 \]

$w$ gives the work that remains to be done and
\[w>0\]

When $w$ reaches $0$ no further work should be done.

\end{itemize}

A program must be written that maintains the following properties:

\begin{itemize}
\item \invariant{P}, that ensures that the partition process is under control;
\item $\eventually w=0$, that ensures that work is being performed by each transition and that eventually no work will be left to be done.
\end{itemize}

In addition, the program must ensure that the bound $w>0$ is respected: progress doesn't get out of control.
When
$w=0$ no more work is performed: a fixpoint has been reached.


The algorithm representing the partitioning of an input vector $S.(0..n-1)$ 
into 4 partitions is depicted in program \ref{splitfst}. It assumes that
$p$ contains the initial index for the splitter. 
It deals with
five conditions on input:
\begin{enumerate}
\item the element pointed to by $lt$ is equal to the splitter: it must be
moved to the right, and this is done through a swap with the element point to
by $nel$;
\item the element pointed to by $lt$ is less than the splitter: $lt$ is advanced;
\item $lt$ and $gt$ point to elements that are respectively greater and less than the splitter: they must be swapped;
\item the analogous for an element equal to the splitter on the right side;
\item $gt$ points to an element greater than the splitter: the pointer moves
to the left.
\end{enumerate}

\begin{bxalgorithm}
\label{splitfst}
\begin{program}
\PROG split
\initially
\ \ sp,nel,lt,ner,gt:=S.p,0,0,n-1,n-1;
\assign
\ \ gt-lt+1>0 \AR \IF S.lt=sp \AR swap(S,nel,lt);
                  \untab\untab\assync\ \ S.lt<sp \AR lt:=lt+1; 
                  \untab\assync\ \ S.lt>sp \pcand S.gt<sp \AR swap(S,lt,gt);
                  \untab\assync\ \ S.gt=sp \AR swap(S,ner,gt);
                  \untab\tab\assync\ \ S.gt>sp \AR gt:=gt-1;
                      \FI
\end{program}
\end{bxalgorithm}

In the algorithm \ref{splitfst}, imagine $swap(S,u,v)$ as an abbreviation
(a macro call) for a code defined as 
\[swap(S,u,v) \DEF S.u,S.v,u,v:=S.v,S.u,u+1,v+1\]

\begin{exercise}
Prove that:
\begin{enumerate}
\item $P$ as defined above is an invariant for program \ref{splitfst}.
\item Given $w$ as above, $\eventually w=0$.
\item Program \ref{splitfst} has a fixpoint.
\item When the fixpoint is reached, the output condition $R$ (defined above) 
is verified.
\end{enumerate}

\end{exercise}

\begin{exercise}
Extend program \ref{splitfst} to move the two partitions with elements equal
to the splitter to center of the vector.
\end{exercise}




\begin{exercise}
Write a program that, given an array $S.(0..n-1)$ of integers, such that the section $S.(0..m-1)$, for   $m<n$, is ordered, orders the section $S.(0..m)$.
\end{exercise}

\begin{exercise}
Extend the program above to order an array  $S.(0..n-1)$.
\end{exercise}

\begin{exercise}
Write a program to find $k-th$ smallest number of a vector $S.(0..n-1)$ of integers.
\end{exercise}

\begin{exercise}
Write a program that, given a sequence $S.(0..n-1)$ of integers, sets a variable
$x$ to the sum of the maximum consecutive subsequence.

\begin{enumerate}
\item State clearly your output condition.
\item Define invariant and bound function.
\item Prove the correctness of your program.

\end{enumerate}

\end{exercise}


\bibliography{abbrev,analysis,formal,algorithms,program}

\bibliographystyle{amsplain}


\end{document}

