documentation: solution for VSTTE'10 problem 3

parent 60ffb6d6
...@@ -153,7 +153,6 @@ why.conf ...@@ -153,7 +153,6 @@ why.conf
/examples/programs/vacid_0_red_black_trees/ /examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/ /examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/ /examples/programs/next_digit_sum/
/examples/programs/vstte10_search_list/
/examples/programs/vstte10_aqueue/ /examples/programs/vstte10_aqueue/
/examples/programs/mergesort_list/ /examples/programs/mergesort_list/
/examples/programs/algo63/ /examples/programs/algo63/
......
...@@ -147,7 +147,7 @@ keyword \texttt{invariant}, immediately after the keyword \texttt{do}. ...@@ -147,7 +147,7 @@ keyword \texttt{invariant}, immediately after the keyword \texttt{do}.
done done
\end{verbatim} \end{verbatim}
There is no need to introduce a variant, as the termination of a There is no need to introduce a variant, as the termination of a
\texttt{for} loop is automatically guaranteed. \texttt{for} loop is automatically guaranteed.
This completes module \texttt{MaxAndSum}. This completes module \texttt{MaxAndSum}.
Figure~\ref{fig:MaxAndSum} shows the whole code. Figure~\ref{fig:MaxAndSum} shows the whole code.
\begin{figure} \begin{figure}
...@@ -294,9 +294,116 @@ end ...@@ -294,9 +294,116 @@ end
\subsection{Problem 3: Searching a Linked List} \subsection{Problem 3: Searching a Linked List}
The third problem is stated as follows:
\begin{quote}
Given a linked list representation of a list of integers,
find the index of the first element that is equal to 0.
\end{quote}
More precisely, the specification says
\begin{quote}
You have to show that the program returns an index $i$ equal to the
length of the list if there is no such element. Otherwise, the $i$-th
element of the list must be equal to 0, and all the preceding
elements must be non-zero.
\end{quote}
Since the list is not mutated, we can use the algebraic data type of
polymorphic lists from \why's standard library, defined in theory
\texttt{list.List}. It comes with other handy theories:
\texttt{list.Length}, which provides a function \texttt{length}, and
\texttt{list.Nth}, which provides a function \texttt{nth}
for the $n$-th element of a list. The latter returns an option type,
depending on whether the index is meaningful or not.
\begin{verbatim}
module SearchingALinkedList
use import int.Int
use export list.List
use export list.Length
use export list.Nth
\end{verbatim}
It is helpful to introduce two predicates: a first one
for a successful search,
\begin{verbatim}
logic zero_at (l: list int) (i: int) =
nth i l = Some 0 and forall j:int. 0 <= j < i -> nth j l <> Some 0
\end{verbatim}
and a another for a non-successful search,
\begin{verbatim}
logic no_zero (l: list int) =
forall j:int. 0 <= j < length l -> nth j l <> Some 0
\end{verbatim}
We are now in position to give the code for the search function.
We write it as a recursive function \texttt{search} which scans a list
for the first zero value:
\begin{verbatim}
let rec search (i: int) (l: list int) = match l with
| Nil -> i
| Cons x r -> if x = 0 then i else search (i+1) r
end
\end{verbatim}
Passing an index \texttt{i} as first argument allows to perform a tail
call. A simpler code (yet less efficient) would return 0 in the first
branch and \texttt{1 + search ...} in the second one, avoiding the
extra argument \texttt{i}.
We first prove the termination of this recursive function. It amounts
to give it a \emph{variant}, that is an term integer term which stays
non-negative and strictly decreases at each recursive call. Here it is
as simple as the length of \texttt{l}:
\begin{verbatim}
let rec search (i: int) (l: list int) variant { length l } = ...
\end{verbatim}
(It is worth pointing out that variants are not limited to natural
numbers. Any other type equipped with a well-founded order relation
can be used instead.)
There is no precondition for function \texttt{search}.
The postcondition expresses that either a zero value is found, and
consequently the value returned is bounded accordingly,
\begin{verbatim}
i <= result < i + length l and zero_at l (result - i)
\end{verbatim}
or no zero value was found, and thus the returned value is exactly
\texttt{i} plus the length of \texttt{l}:
\begin{verbatim}
result = i + length l and no_zero l
\end{verbatim}
Solving the problem is simply a matter of calling \texttt{search} with
0 as first argument.
The code is given Figure~\ref{fig:LinkedList}. The verification
conditions are all discharged automatically.
\begin{figure} \begin{figure}
\centering \centering
\begin{verbatim} \begin{verbatim}
module SearchingALinkedList
use import int.Int
use export list.List
use export list.Length
use export list.Nth
logic zero_at (l: list int) (i: int) =
nth i l = Some 0 and forall j:int. 0 <= j < i -> nth j l <> Some 0
logic no_zero (l: list int) =
forall j:int. 0 <= j < length l -> nth j l <> Some 0
let rec search (i: int) (l: list int) variant { length l } =
{}
match l with
| Nil -> i
| Cons x r -> if x = 0 then i else search (i+1) r
end
{ (i <= result < i + length l and zero_at l (result - i))
or
(result = i + length l and no_zero l) }
let search_list (l: list int) =
{ }
search 0 l
{ (0 <= result < length l and zero_at l result)
or
(result = length l and no_zero l) }
end
\end{verbatim} \end{verbatim}
\hrulefill \hrulefill
\caption{Solution for VSTTE'10 competition problem 3.} \caption{Solution for VSTTE'10 competition problem 3.}
......
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html (* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 3: searching a linked list *) Problem 3: searching a linked list *)
module M module SearchingALinkedList
use import int.Int use import int.Int
use import module ref.Ref
use export list.List use export list.List
use export list.Length use export list.Length
use export list.Nth use export list.Nth
logic zero_at (l : list int) (i : int) = logic zero_at (l: list int) (i: int) =
nth i l = Some 0 and forall j:int. 0 <= j < i -> nth j l <> Some 0 nth i l = Some 0 and forall j:int. 0 <= j < i -> nth j l <> Some 0
logic no_zero (l : list int) = logic no_zero (l: list int) =
forall j:int. 0 <= j < length l -> nth j l <> Some 0 forall j:int. 0 <= j < length l -> nth j l <> Some 0
let rec search i l variant { length l } = let rec search (i: int) (l: list int) variant { length l } =
{} {}
match l with match l with
| Nil -> i | Nil -> i
...@@ -25,7 +24,7 @@ module M ...@@ -25,7 +24,7 @@ module M
or or
(result = i + length l and no_zero l) } (result = i + length l and no_zero l) }
let search_list l = let search_list (l: list int) =
{ } { }
search 0 l search 0 l
{ (0 <= result < length l and zero_at l result) { (0 <= result < length l and zero_at l result)
...@@ -35,6 +34,7 @@ module M ...@@ -35,6 +34,7 @@ module M
(* imperative version, with a loop *) (* imperative version, with a loop *)
use import module ref.Ref
use import list.HdTl use import list.HdTl
let head (l : list 'a) = let head (l : list 'a) =
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/vstte10_search_list/why3session.xml">
<file name="../vstte10_search_list.mlw" verified="false" expanded="true">
<theory name="SearchingALinkedList" verified="false" expanded="true">
<goal name="WP_parameter search" expl="correctness of parameter search" sum="0f056b7e2d8ac0af82fd9fa38702f209" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal name="WP_parameter search_list" expl="normal postcondition" sum="9e1415eb87291fae526a464eef8b7f8c" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter head" expl="correctness of parameter head" sum="cdcac13c1814691e488082e128de305f" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter tail" expl="correctness of parameter tail" sum="c8d4a6c630e6f2e6c1c583712e86297c" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop" expl="correctness of parameter search_loop" sum="bed538740c5efbe540217617f91af77f" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="true">
<result status="unknown" time="1.31"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter search_loop.1" expl="loop invariant init" sum="bd0b0078bb630c57cd14044638c9c0cc" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.2" expl="precondition" sum="00d6259354783962f481093aa81e5e4d" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.3" expl="precondition" sum="d3d6320ebf6ee20ecd580a675d8610b2" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.4" expl="loop invariant preservation" sum="aa15309cc5737a6281b66d9f01ff51d7" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="unknown" time="0.92"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.5" expl="loop variant decreases" sum="fc86b9ce14a19d940300c547eec9a8e1" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter search_loop.5.1" expl="correctness of parameter search_loop" sum="95d0f5d73a20a5cd7333750c975d2c2c" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.5.2" expl="correctness of parameter search_loop" sum="82cd009cc290bbeb5f7ebd291a2dfc42" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter search_loop.6" expl="normal postcondition" sum="d01b1212c0ab3708ed70ad837bb1929c" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="unknown" time="0.13"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.7" expl="precondition" sum="08abb0e6f24d0611e8508cd7c0d2fe64" proved="true" expanded="false">
<proof prover="cvc3" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.8" expl="loop invariant preservation" sum="b2299f8763b01027943b66ab59813853" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.9" expl="loop variant decreases" sum="24359c547c53547ed5631c8c5ba2e811" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.10" expl="normal postcondition" sum="0c5ffbc474072205a10fd50af67f1bec" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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