\documentclass[12pt]{amsart}
\usepackage{pvs}
\usepackage{alltt}
\usepackage{boxedminipage}    
\input{defcode}
\input{defalgo}
\usepackage{program}
\def\unity{\textbf{UNITY}}
\def\pvs{\textbf{PVS}}

\title{PVS: describing and validating algorithms \\ 
A clumsy try \\
Very drafty}

\author{Raul H.C.Lopes}
\begin{document}

\section{Introduction}
This draft presents an introduction to the use of \pvs\ for validating
algorithms.


\begin{verbatim}
./tex2code.pl < logicalalgo.tex 
\end{verbatim}


\section{The maximum of a set of numbers}
An algorithm for computing the maximum of a set of numbers is presented 
in \cite{misra:unity94}. Misra presents both operational and non-operational 
descriptions for that same algorithm, using the logic of \unity.
That description essentially establishes relation between the states
of program to be defined. That description is reproduced below, followed
by a \pvs\ encoding of it.

\section{A \unity\ description}

\emph{Fact:} An execution of a program can be represented as a 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}\]

that for any action of the system in a state where $p$ holds,
a new state will result where $q$ will hold.

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 given in \ref{maxlogical}. Notice
the use of the 
operator {\bf co} described above. 

\begin{bxalgorithm}
\label{maxlogical}
\begin{program}
\PROG max
\initially\ v=0
\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=0$

Before any computation $v$ must be initialized to $0$.

\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}

Property $\alpha$ is a safety property: $v$ never decreases and, when it changes, it moves to a new value from $S$.

Property $\beta$ ensures progress. It wouldn't help if $v$ wad initiallized to
$0$ and then never changed. $\alpha$ would still hold, but the maximun in 
$S$ would never be obtained. $\beta$ enforces that $S$ will be completely
scanned: eventually any value
in $S$ will have been compared to $v$.

\section{A \pvs\ description}

The algorithm is coded here as \pvs\ theory. 
The first  line defines that the theory is called \emph{max}.

\begin{code}%file: max.pvs

max : THEORY
  BEGIN
\end{code}

Next two lines define:
\begin{itemize}
\item\textbf{v}: that identify the maximum at the end of computation.
\item\textbf{S}: the set whose maximum is being searched.
\end{itemize}

\fvset{firstnumber=last}
\begin{code}%file: max.pvs

  v : nat;
  S  : setof[nat];
\end{code}

\unity's \textbf{co} operator relates a state with its successor. A state
will be understood as a map from variables to values \cite{lamport:tla}.
However, because \pvs\ doesn't have temporal operators, and a relation
on sequences of states must be expressed, the concept of state will 
be modeled through a function mapping pairs of integers to integers:
\begin{itemize}
\item\textbf{st} represents the state function. Given a non-negative integer
representing the states (states are numbered from $0$), and the variable
$v$ (another non-negative integer), it returns the value of $v$ in the
respective state.
\end{itemize}
\begin{code}%file: max.pvs

  st : [nat,nat->nat];
\end{code}

The axiom \textbf{INIT} defines the initial state (thus, $0$) of the computation. In state $0$, $v$ has value $0$.

\begin{code}%file: max.pvs

  INIT: AXIOM st(0,v)=0;
\end{code}

Axiom \textbf{NEXT} relates the value of $v$ in state $i$ (say $m$) to
its value in the succeeding state ($i+1$), which must be either $m$ or
some number greater than $m$ and contained in $S$.

\begin{code}%file: max.pvs

  NEXT: AXIOM forall (i:nat,m:nat): 
		st(i,v)=m IMPLIES 
                   (st(i+1,v)=m OR 
	              (st(i+1,v)>m AND S(st(i+1,v))))
\end{code}

The progress condition is represented by the axiom \textbf{PROG}.
\begin{code}%file: max.pvs
 
  PROG: AXIOM forall (i:nat, m:nat):
                exists (j:nat):
                 (j >= i) AND
                  (m IN S IMPLIES st(

Next the \emph{formula} \textbf{STABLE} is introduced. A formula is a conjecture that must be proved. This conjecture in particular states a \emph{stability}
property: that if $v$ is greater than some $n$ in a state, it will still
be grater than $n$ in the succeeding state.
 
\begin{code}%file: max.pvs

  STABLE: FORMULA forall(i:nat,n:nat): st(i,v)>=n IMPLIES 
                                         st(i+1,v)>=n

 
END max

\end{code}

The \pvs\ proof follows.
\input{STABLE}

\section{A first abstract data type} 

\begin{code}%file: stacks.pvs

stacks [t: TYPE+] : THEORY
  BEGIN

  stack : TYPE+
  s : VAR stack
  empty : stack
  nonemptystack?(s) : bool = s /= empty
  nonemptystack_exists: AXIOM EXISTS s: nonemptystack?(s)

  push: [t, stack -> (nonemptystack?)]
  pop: [(nonemptystack?) -> stack]
  top: [(nonemptystack?) -> t]

  x,y: VAR t

  push_top_pop: AXIOM
    nonemptystack?(s) IMPLIES push(top(s), pop(s)) = s

  pop_push: AXIOM pop(push(x, s)) = s

  top_push: AXIOM top(push(x, s)) = x

  pop2push2: THEOREM pop(pop(push(x, push(y, s)))) = push(y,s) 

END stacks 

\end{code}

\bibliography{abbrev,os,analysis,formal,algorithms,program}
 
\bibliographystyle{amsplain} 
\end{document}
