Skip to content

why3
why3
Commit 60ffb6d6 authored by Jean-Christophe Filliatre's avatar Jean-Christophe Filliatre
Browse files
Options

documentation: solution for VSTTE'10 problem 2

parent b50d24d9
Hide whitespace changes
Inline Side-by-side
Showing with 311 additions and 10 deletions
doc/whyml.tex
View file @ 60ffb6d6
......@@ -49,6 +49,8 @@ See Chapter~\ref{chap:manpages} for more details regarding command lines.
\medskip
As an introduction to \whyml, we use the five problems from the VSTTE
2010 verification competition~\cite{vstte10comp}.
The source code for all these examples is contained in \why's
distribution, in dub-directory \texttt{examples/programs/}.
\subsection{Problem 1: Sum and Maximum}
......@@ -192,9 +194,98 @@ Coq, and thus completes the verification.
\subsection{Problem 2: Inverting an Injection}
The second problem is stated as follows:
\begin{quote}
Invert an injective array $A$ on $N$ elements in the
subrange from $0$ to $N - 1$, i.e., the output array $B$ must be
such that $B[A[i]] = i$ for $0 \le i < N$.
\end{quote}
We may assume that $A$ is surjective and we have to prove
that the resulting array is also injective.
The code is immediate, since it is as simple as
\begin{verbatim}
for i = 0 to n - 1 do b[a[i]] <- i done
\end{verbatim}
so it is more a matter of specification and of getting the proof done
with as much automation as possible. In a new file, we start a new
module and we import arithmetic and arrays:
\begin{verbatim}
module InvertingAnInjection
use import int.Int
use import module array.Array
\end{verbatim}
It is convenient to introduce predicate definitions for the properties
of being injective and surjective. These are purely logical
declarations:
\begin{verbatim}
logic injective (a: array int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
logic surjective (a: array int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n and a[j] = i)
\end{verbatim}
It is also convenient to introduce the predicate ``being in the
subrange from 0 to $n-1$'':
\begin{verbatim}
logic range (a: array int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
\end{verbatim}
Using these predicates, we can formulate the assumption that any
injective array of size $n$ within the range $0..n-1$ is also surjective:
\begin{verbatim}
lemma injective_surjective:
forall a: array int, n: int.
injective a n -> range a n -> surjective a n
\end{verbatim}
We declare it as a lemma rather than as an axiom, since it is actually
provable. It requires induction and can be proved using the Coq proof
assistant for instance.
Finally we can give the code a specification, with a loop invariant
which simply expresses the values assigned to array \texttt{b} so far:
\begin{verbatim}
let inverting (a: array int) (b: array int) (n: int) =
{ 0 <= n = length a = length b and injective a n and range a n }
for i = 0 to n - 1 do
invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
b[a[i]] <- i
done
{ injective b n }
\end{verbatim}
Here we chose to have array \texttt{b} as argument; returning a
freshly allocated array would be equally simple.
The whole module is given Figure~\ref{fig:Inverting}.
The verification conditions for function \texttt{inverting} are easily
discharged automatically, thanks to the lemma.
\begin{figure}
\centering
\begin{verbatim}
module InvertingAnInjection
use import int.Int
use import module array.Array
logic injective (a: array int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
logic surjective (a: array int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n and a[j] = i)
logic range (a: array int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
lemma injective_surjective:
forall a: array int, n: int.
injective a n -> range a n -> surjective a n
let inverting (a: array int) (b: array int) (n: int) =
{ 0 <= n = length a = length b and injective a n and range a n }
for i = 0 to n - 1 do
invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
b[a[i]] <- i
done
{ injective b n }
end
\end{verbatim}
\hrulefill
\caption{Solution for VSTTE'10 competition problem 2.}
......@@ -237,7 +328,10 @@ Coq, and thus completes the verification.
% other examples: same fringe ?
%%% Local Variables:
%%% compile-command: "make -C .. doc"
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
% LocalWords: surjective
examples/programs/vstte10_inverting.mlw
View file @ 60ffb6d6
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 2: inverting an injection *)
module M
module InvertingAnInjection
use import int.Int
use import module array.Array
......@@ -10,25 +10,81 @@ module M
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
logic surjective (a: array int) (n: int) =
forall i: int [i]. 0 <= i < n -> exists j: int. (0 <= j < n and a[j] = i)
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n and a[j] = i)
logic range (a: array int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
lemma Injective_surjective:
lemma injective_surjective:
forall a: array int, n: int.
injective a n -> range a n -> surjective a n
let inverting (a: array int) (b: array int) n =
{ n >= 0 and length a = n and length b = n and
injective a n and range a n }
for i = 0 to n-1 do
invariant
{ length b = n and forall j: int. 0 <= j < i -> b[a[j]] = j }
b[a[i]] <- i
let inverting (a: array int) (b: array int) (n: int) =
{ 0 <= n = length a = length b and injective a n and range a n }
for i = 0 to n - 1 do
invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
b[a[i]] <- i
done
{ injective b n }
(* variant where array b is returned and with additional post *)
let inverting2 (a: array int) (n: int) =
{ 0 <= n = length a and injective a n and range a n }
let b = make n 0 in
for i = 0 to n - 1 do
invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
b[a[i]] <- i
done;
b
{ length result = n and injective result n and
forall i: int. 0 <= i < n -> result[a[i]] = i }
end
module Test
use import module array.Array
use import module InvertingAnInjection
let test () =
let a = make 10 0 in
a[0] <- 9;
a[1] <- 3;
a[2] <- 8;
a[3] <- 2;
a[4] <- 7;
a[5] <- 4;
a[6] <- 0;
a[7] <- 1;
a[8] <- 5;
a[9] <- 6;
assert {
a[0] = 9 &&
a[1] = 3 &&
a[2] = 8 &&
a[3] = 2 &&
a[4] = 7 &&
a[5] = 4 &&
a[6] = 0 &&
a[7] = 1 &&
a[8] = 5 &&
a[9] = 6
};
let b = inverting2 a 10 in
assert {
b[0] = 6 &&
b[1] = 7 &&
b[2] = 3 &&
b[3] = 1 &&
b[4] = 5 &&
b[5] = 8 &&
b[6] = 9 &&
b[7] = 4 &&
b[8] = 2 &&
b[9] = 0
}
end
(*
......
examples/programs/vstte10_inverting/why3session.xml 0 → 100644
View file @ 60ffb6d6
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/vstte10_inverting/why3session.xml">
<file name="../vstte10_inverting.mlw" verified="false" expanded="true">
<theory name="InvertingAnInjection" verified="false" expanded="true">
<goal name="injective_surjective" sum="fef9aae58c36b286dc28a42bba27502f" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="unknown" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter inverting" expl="correctness of parameter inverting" sum="accce61cb6e55257c9d64b39707667e8" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter inverting.1" expl="normal postcondition" sum="0b317d7160748b850c2e9d12db9c11c7" 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 inverting.2" expl="for loop initialization" sum="801c23980d4fe475e8b394392eb4785f" 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 inverting.3" expl="for loop preservation" sum="0be2a7cb2d3ca0e8249532bc6e102fc9" proved="true" expanded="false">
<proof prover="cvc3" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter inverting.4" expl="normal postcondition" sum="908d6f320df48198da298e5533eb9995" proved="true" expanded="false">
<proof prover="z3" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter inverting2" expl="correctness of parameter inverting2" sum="841741738d6103b53e6e75326b605da6" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter inverting2.1" expl="normal postcondition" sum="0ae2f8127381722654e3bc5999215095" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter inverting2.2" expl="for loop initialization" sum="c28611c680020848cf41b776e30b46f2" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter inverting2.3" expl="for loop preservation" sum="afc170e6aae06fbdd78f4d205be72cc4" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter inverting2.4" expl="normal postcondition" sum="b5b0b5d4a3a5a1e60e6ab3c196bd7860" proved="true" expanded="false">
<proof prover="z3" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Test" verified="true" expanded="false">
<goal name="WP_parameter test" expl="correctness of parameter test" sum="301187f85f12a299cb0fd1acdb7a9880" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter test.1" expl="precondition" sum="a5614a4274bae2ae78dac6edebc488a9" 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 test.2" expl="precondition" sum="db5b7a72cbc8b333b02c9f2677151e6b" 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 test.3" expl="precondition" sum="5961fdcea4c073324c33aed15a2c0768" 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 test.4" expl="precondition" sum="cc5b2b45ffb55cdbbe6e6e1f0d989c92" 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 test.5" expl="precondition" sum="50df2ea6b3656f3e998e0fa966aaa827" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter test.6" expl="precondition" sum="a29a8c0cae3803d10badf88a70d9b081" 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 test.7" expl="precondition" sum="748b842c66760936ded4a474ab503b35" 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 test.8" expl="precondition" sum="ae1ea6e7c9fec7b8f3cdd56c6b27c691" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter test.9" expl="precondition" sum="82fd8241bb7b8bebdb12f14b97663b0d" 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 test.10" expl="precondition" sum="ecf7135af52187cf60e4e9b3ba6170ba" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter test.11" expl="assertion" sum="21e0b9f37b4396ac423f462de2d51089" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.15"/>
</proof>
</goal>
<goal name="WP_parameter test.12" expl="precondition" sum="be53ca6d295c6cdd6e56d9722d29ad79" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter test.12.1" expl="correctness of parameter test" sum="d664b57b3382a611b68743240da1a14c" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter test.12.2" expl="correctness of parameter test" sum="e748d316e5ec52b5de05f54561e6a9e8" 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 test.12.3" expl="correctness of parameter test" sum="4dd3751bdfc9e50ba21a4fae001089fd" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.27"/>
</proof>
</goal>
<goal name="WP_parameter test.12.4" expl="correctness of parameter test" sum="169562534e5f509faababb235ae227c1" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.18"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter test.13" expl="assertion" sum="5936d88780435fa5ea7f67b871ac40d6" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</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