documentation: solution for VSTTE'10 problem 5

parent 5fac9dc8
......@@ -153,7 +153,6 @@ why.conf
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/vstte10_aqueue/
/examples/programs/mergesort_list/
/examples/programs/algo63/
/examples/programs/algo64/
......
......@@ -196,3 +196,9 @@
address = {Edinburgh, Scotland},
note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}}
@BOOK{okasaki98,
author = {Chris Okasaki},
title = {{Purely Functional Data Structures}},
publisher = {Cambridge University Press},
year = 1998
}
......@@ -173,7 +173,7 @@ module MaxAndSum
end
\end{verbatim}
\hrulefill
\vspace*{-2em}\hrulefill
\caption{Solution for VSTTE'10 competition problem 1.}
\label{fig:MaxAndSum}
\end{figure}
......@@ -287,7 +287,7 @@ module InvertingAnInjection
end
\end{verbatim}
\hrulefill
\vspace*{-2em}\hrulefill
\caption{Solution for VSTTE'10 competition problem 2.}
\label{fig:Inverting}
\end{figure}
......@@ -405,7 +405,7 @@ module SearchingALinkedList
end
\end{verbatim}
\hrulefill
\vspace*{-2em}\hrulefill
\caption{Solution for VSTTE'10 competition problem 3.}
\label{fig:LinkedList}
\end{figure}
......@@ -470,18 +470,186 @@ the loop invariant.
\centering
\begin{verbatim}
\end{verbatim}
\hrulefill
\vspace*{-2em}\hrulefill
\caption{Solution for VSTTE'10 competition problem 4.}
\label{fig:NQueens}
\end{figure}
\subsection{Problem 5: Amortized Queue}
The last problem consists in verifying the implementation of a
well-known purely applicative data structure for queues.
A queue is composed of two lists, \textit{front} and \textit{rear}.
We push elements at the head of list \textit{rear} and pop them off
the head of list \textit{front}. We maintain that the length of
\textit{front} is always greater or equal to the length of \textit{rear}.
(See for instance Okasaki's \emph{Purely Functional Data
Structures}~\cite{okasaki98} for more details.)
We have to implement operations \texttt{empty}, \texttt{head},
\texttt{tail}, and \texttt{enqueue} over this data type,
to show that the invariant over lengths is maintained, and finally
\begin{quote}
to show that a client invoking these operations
observes an abstract queue given by a sequence.
\end{quote}
In a new module, we import arithmetic and theory
\texttt{list.ListRich}, a combo theory which imports all list
operations we will require: length, reversal, and concatenation.
\begin{verbatim}
module AmortizedQueue
use import int.Int
use export list.ListRich
\end{verbatim}
The queue data type is naturally introduced as a polymorphic record type.
The two list lengths are explicitly stored, for better efficiency.
\begin{verbatim}
type queue 'a = {| front: list 'a; lenf: int;
rear : list 'a; lenr: int; |}
\end{verbatim}
We start with the definition of the data type invariant, as a
predicate \texttt{inv}. It makes use of the ability to chain
several equalities and inequalities.
\begin{verbatim}
logic inv (q: queue 'a) =
length q.front = q.lenf >= length q.rear = q.lenr
\end{verbatim}
For the purpose of the specification, it is convenient to introduce a function
\texttt{sequence} which builds the sequence of a queue elements, that
is the front list concatenated to reversed rear list.
\begin{verbatim}
logic sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear
\end{verbatim}
It is worth pointing out that this function will only be used in
specifications.
We start with the easiest operation: building the empty queue.
\begin{verbatim}
let empty () =
{}
{| front = Nil; lenf = 0; rear = Nil; lenr = 0 |} : queue 'a
{ inv result and sequence result = Nil }
\end{verbatim}
The postcondition is twofold: the returned queue satisfies its
invariant and represents the empty sequence.
Note the cast to type \texttt{queue 'a}. It is required, for the
type checker not to complain about an undefined type variable.
The next operation is \texttt{head}, which returns the first element from
a given queue \texttt{q}. It naturally requires the queue to be non
empty, which is conveniently expressed as \texttt{sequence q} not
being \texttt{Nil}.
\begin{verbatim}
let head (q: queue 'a) =
{ inv q and sequence q <> Nil }
match q.front with
| Nil -> absurd
| Cons x _ -> x
end
{ hd (sequence q) = Some result }
\end{verbatim}
Note the presence of the invariant in the precondition, which is
required to prove the absurdity of the first branch (if
\texttt{q.front} is \texttt{Nil}, then so should be \texttt{sequence q}).
The next operation is \texttt{tail}, which removes the first element
from a given queue. This is more subtle than \texttt{head}, since we
may have to re-structure the queue to maintain the invariant.
Since we will have to perform a similar operation when implementation
operation \texttt{enqueue}, it is a good idea to introduce a smart
constructor \texttt{create} which builds a queue from two lists, while
ensuring the invariant. The list lengths are also passed as arguments,
to avoid unnecessary computations.
\begin{verbatim}
let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) =
{ lf = length f and lr = length r }
if lf >= lr then
{| front = f; lenf = lf; rear = r; lenr = lr |}
else
let f = f ++ reverse r in
{| front = f; lenf = lf + lr; rear = Nil; lenr = 0 |}
{ inv result and sequence result = f ++ reverse r }
\end{verbatim}
If the invariant already holds, it is simply a matter of building the
record. Otherwise, we empty the rear list and build a new front list
as the concatenation of list \texttt{f} and the reversal of list \texttt{r}.
The principle of this implementation is that the cost of this reversal
will be amortized over all queue operations. Implementing function
\texttt{tail} is now straightforward and follows the structure of
function \texttt{head}.
\begin{verbatim}
let tail (q: queue 'a) =
{ inv q and sequence q <> Nil }
match q.front with
| Nil -> absurd
| Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
end
{ inv result and tl (sequence q) = Some (sequence result) }
\end{verbatim}
The last operation is \texttt{enqueue}, which pushes a new element in
a given queue. Reusing the smart constructor \texttt{create} makes it
a one line code.
\begin{verbatim}
let enqueue (x: 'a) (q: queue 'a) =
{ inv q }
create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
{ inv result and sequence result = sequence q ++ Cons x Nil }
\end{verbatim}
The code is given Figure~\ref{fig:AQueue}. The verification conditions
are all discharged automatically.
\begin{figure}
\centering
\begin{verbatim}
module AmortizedQueue
use import int.Int
use export list.ListRich
type queue 'a = {| front: list 'a; lenf: int;
rear : list 'a; lenr: int; |}
logic inv (q: queue 'a) =
length q.front = q.lenf >= length q.rear = q.lenr
logic sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear
let empty () =
{}
{| front = Nil; lenf = 0; rear = Nil; lenr = 0 |} : queue 'a
{ inv result and sequence result = Nil }
let head (q: queue 'a) =
{ inv q and sequence q <> Nil }
match q.front with
| Nil -> absurd
| Cons x _ -> x
end
{ hd (sequence q) = Some result }
let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) =
{ lf = length f and lr = length r }
if lf >= lr then
{| front = f; lenf = lf; rear = r; lenr = lr |}
else
let f = f ++ reverse r in
{| front = f; lenf = lf + lr; rear = Nil; lenr = 0 |}
{ inv result and sequence result = f ++ reverse r }
let tail (q: queue 'a) =
{ inv q and sequence q <> Nil }
match q.front with
| Nil -> absurd
| Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
end
{ inv result and tl (sequence q) = Some (sequence result) }
let enqueue (x: 'a) (q: queue 'a) =
{ inv q }
create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
{ inv result and sequence result = sequence q ++ Cons x Nil }
end
\end{verbatim}
\hrulefill
\vspace*{-2em}\hrulefill
\caption{Solution for VSTTE'10 competition problem 5.}
\label{fig:AQueue}
\end{figure}
......
module M
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 5: amortized queue *)
module AmortizedQueue
use import int.Int
use export list.ListRich
type queue 'a = Q (front : list 'a) (lenf : int)
(rear : list 'a) (lenr : int)
logic inv (q : queue 'a) =
length (front q) = lenf q and
length (rear q) = lenr q and
lenf q >= lenr q
logic model (q : queue 'a) : list 'a =
front q ++ reverse (rear q)
let create f lf r lr =
{ lf = length f and lr = length r }
if lf >= lr then
Q f lf r lr
else
let f = f ++ reverse r in
Q f (lf + lr) Nil 0
: queue 'a
{ inv result and model result = f ++ reverse r }
let empty () =
{}
Q Nil 0 Nil 0 : queue 'a
{ inv result and model result = Nil }
let head (q : queue 'a) =
{ inv q and model q <> Nil }
match front q with
| Nil -> absurd
| Cons x _ -> x
end
{ hd (model q) = Some result }
let tail (q : queue 'a) =
{ inv q and model q <> Nil }
match front q with
| Nil -> absurd
| Cons _ r -> create r (lenf q - 1) (rear q) (lenr q)
end
{ inv result and tl (model q) = Some (model result) }
let enqueue (x : 'a) (q : queue 'a) =
{ inv q }
create (front q) (lenf q) (Cons x (rear q)) (lenr q + 1)
{ inv result and model result = model q ++ Cons x Nil }
type queue 'a = {| front: list 'a; lenf: int;
rear : list 'a; lenr: int; |}
logic inv (q: queue 'a) =
length q.front = q.lenf >= length q.rear = q.lenr
logic sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear
let empty () =
{}
{| front = Nil; lenf = 0; rear = Nil; lenr = 0 |} : queue 'a
{ inv result and sequence result = Nil }
let head (q: queue 'a) =
{ inv q and sequence q <> Nil }
match q.front with
| Nil -> absurd
| Cons x _ -> x
end
{ hd (sequence q) = Some result }
let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) =
{ lf = length f and lr = length r }
if lf >= lr then
{| front = f; lenf = lf; rear = r; lenr = lr |}
else
let f = f ++ reverse r in
{| front = f; lenf = lf + lr; rear = Nil; lenr = 0 |}
{ inv result and sequence result = f ++ reverse r }
let tail (q: queue 'a) =
{ inv q and sequence q <> Nil }
match q.front with
| Nil -> absurd
| Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
end
{ inv result and tl (sequence q) = Some (sequence result) }
let enqueue (x: 'a) (q: queue 'a) =
{ inv q }
create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
{ inv result and sequence result = sequence q ++ Cons x Nil }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_aqueue.gui"
End:
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/vstte10_aqueue/why3session.xml">
<file name="../vstte10_aqueue.mlw" verified="true" expanded="true">
<theory name="AmortizedQueue" verified="true" expanded="true">
<goal name="WP_parameter create" expl="correctness of parameter create" sum="94603ee07e585f398458946ecc7a0f0b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal name="WP_parameter empty" expl="normal postcondition" sum="3612f3c6fbb172a8f7bb557de13fd5b0" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter head" expl="correctness of parameter head" sum="9cf1d7ca07c9a4889ad2822b0d4f8851" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter tail" expl="correctness of parameter tail" sum="7b2a5c6b28da9c887812b2ba52dd88bc" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter tail.1" expl="correctness of parameter tail" sum="cb15b2861f2bd1dc0448b73df780ef7d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter tail.2" expl="correctness of parameter tail" sum="bc0304b50128f3903bde1f29727f0e10" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter tail.3" expl="correctness of parameter tail" sum="5fa5c35fd62cc45245331750d880c0c9" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.17"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter enqueue" expl="correctness of parameter enqueue" sum="942866fdebad37c06e3ffcf86fc15a92" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -269,7 +269,7 @@ theory ListRich
end
(*
Local Variables:
Local Variables:
compile-command: "make -C .. theories/list"
End:
End:
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment