documentation: solution for VSTTE'10 problem 1

parent 7cc748ed
...@@ -63,16 +63,177 @@ and we have to prove the following postcondition: ...@@ -63,16 +63,177 @@ and we have to prove the following postcondition:
\begin{displaymath} \begin{displaymath}
sum \le N \times max. sum \le N \times max.
\end{displaymath} \end{displaymath}
In a file \verb|max_sum.mlw|, we start a new module:
\begin{verbatim}
module MaxAndSum
\end{verbatim}
We are obviously needing arithmetic, so we import the corresponding
theory, exactly as we would do within a theory definition:
\begin{verbatim}
use import int.Int
\end{verbatim}
We are also going to use references and arrays from \whyml's standard
library, so we import the corresponding modules, with a similar
declaration:
\begin{verbatim}
use import module ref.Ref
use import module array.Array
\end{verbatim}
The additional keyword \texttt{module} means that we are looking for
\texttt{.mlw} files from the standard library (namely \texttt{ref.mlw}
and \texttt{array.mlw} here), instead of \texttt{.why} files.
Modules \texttt{Ref} and \texttt{Array} respectively provide a type
\texttt{ref 'a} for references and a type \texttt{array 'a} for
arrays (see Chapter~\ref{chap:mllibrary}), together with useful
operations and traditional syntax.
We are now in position to define a program function
\verb|max\_sum|. A function definition is introduced with the keyword
\texttt{let}. In our case, it introduces a function with two argument,
an array \texttt{a} and its size \texttt{n}:
\begin{verbatim}
let max_sum (a: array int) (n: int) = ...
\end{verbatim}
(There is a function \texttt{length} to get the size of an array but
we add this extra parameter \texttt{n} to stay close to the original
problem statement.) The function body is a Hoare triple, that is a
precondition, a program expression, and a postcondition.
\begin{verbatim}
let max_sum (a: array int) (n: int) =
{ 0 <= n = length a and forall i:int. 0 <= i < n -> a[i] >= 0 }
... expression ...
{ let (sum, max) = result in sum <= n * max }
\end{verbatim}
The precondition expresses that \texttt{n} is non-negative and is
equal to the length of \texttt{a} (this will be needed for
verification conditions related to array bound checking), and that all
elements of \texttt{a} are non-negative.
The postcondition assumes that the value returned by the function,
denoted \texttt{result}, is a pair of integers, and decomposes it as
the pair \texttt{(sum, max)} to expresse the required property.
We are now left with the function body itself, that is a code
computing the sum and the maximum of all elements in \texttt{a}. With
no surpise, it is as simple as introducing two local references
\begin{verbatim}
let sum = ref 0 in
let max = ref 0 in
\end{verbatim}
scanning the array with a \texttt{for} loop, updating \texttt{max}
and \texttt{sum}
\begin{verbatim}
for i = 0 to n - 1 do
if !max < a[i] then max := a[i];
sum := !sum + a[i]
done;
\end{verbatim}
and finally returning the pair of the values contained in \texttt{sum}
and \texttt{max}:
\begin{verbatim}
(!sum, !max)
\end{verbatim}
This completes the code for function \texttt{max\_sum}.
As such, it cannot be proved correct, since the loop is still lacking
a loop invariant. In this case, the loop invariant is as simple as
\verb|!sum <= i * !max|, since the postcondition only requires to prove
\verb|sum <= n * max|. The loop invariant is introduced with the
keyword \texttt{invariant}, immediately after the keyword \texttt{do}.
\begin{verbatim}
for i = 0 to n - 1 do
invariant { !sum <= i * !max }
...
done
\end{verbatim}
There is no need to introduce a variant, as the termination of a
\texttt{for} loop is automatically guaranteed.
This completes module \texttt{MaxAndSum}.
Figure~\ref{fig:MaxAndSum} shows the whole code.
\begin{figure}
\centering
\begin{verbatim}
module MaxAndSum
use import int.Int
use import module ref.Ref
use import module array.Array
let max_sum (a: array int) (n: int) =
{ 0 <= n = length a and forall i:int. 0 <= i < n -> a[i] >= 0 }
let sum = ref 0 in
let max = ref 0 in
for i = 0 to n - 1 do
invariant { !sum <= i * !max }
if !max < a[i] then max := a[i];
sum := !sum + a[i]
done;
(!sum, !max)
{ let (sum, max) = result in sum <= n * max }
end
\end{verbatim}
\hrulefill
\caption{Solution for VSTTE'10 competition problem 1.}
\label{fig:MaxAndSum}
\end{figure}
We can now proceed to its verification.
Running \texttt{why3ml}, or better \texttt{why3ide}, on file
\verb|max_sum.mlw| will show a single verification condition with name
\verb|WP_parameter_max_sum|.
Discharging this verification condition with an automated theorem
prover will not succeed, most likely, as it involves non-linear
arithmetic. Repeated applications of goal splitting and calls to
SMT solvers (within \texttt{why3ide}) will typically leave a single,
unsolved goal, which reduces to proving the following sequent:
\begin{displaymath}
s \le i \times max, ~ max < a[i] \vdash s + a[i] \le (i+1) \times a[i].
\end{displaymath}
This is easily discharged using an interactive proof assistant such as
Coq, and thus completes the verification.
\subsection{Problem 2: Inverting an Injection} \subsection{Problem 2: Inverting an Injection}
\begin{figure}
\centering
\begin{verbatim}
\end{verbatim}
\hrulefill
\caption{Solution for VSTTE'10 competition problem 2.}
\label{fig:Inverting}
\end{figure}
\subsection{Problem 3: Searching a Linked List} \subsection{Problem 3: Searching a Linked List}
\begin{figure}
\centering
\begin{verbatim}
\end{verbatim}
\hrulefill
\caption{Solution for VSTTE'10 competition problem 3.}
\label{fig:LinkedList}
\end{figure}
\subsection{Problem 4: N-Queens} \subsection{Problem 4: N-Queens}
\begin{figure}
\centering
\begin{verbatim}
\end{verbatim}
\hrulefill
\caption{Solution for VSTTE'10 competition problem 4.}
\label{fig:NQueens}
\end{figure}
\subsection{Problem 5: Amortized Queue} \subsection{Problem 5: Amortized Queue}
\begin{figure}
\centering
\begin{verbatim}
\end{verbatim}
\hrulefill
\caption{Solution for VSTTE'10 competition problem 5.}
\label{fig:AQueue}
\end{figure}
% other examples: same fringe ? % other examples: same fringe ?
%%% Local Variables: %%% Local Variables:
......
...@@ -8,12 +8,11 @@ module MaxAndSum ...@@ -8,12 +8,11 @@ module MaxAndSum
use import module array.Array use import module array.Array
let max_sum (a: array int) (n: int) = let max_sum (a: array int) (n: int) =
{ n >= 0 and length a = n and forall i:int. 0 <= i < n -> a[i] >= 0 } { 0 <= n = length a and forall i:int. 0 <= i < n -> a[i] >= 0 }
let sum = ref 0 in let sum = ref 0 in
let max = ref 0 in let max = ref 0 in
for i = 0 to n - 1 do for i = 0 to n - 1 do
invariant invariant { !sum <= i * !max }
{ !sum <= i * !max and forall j:int. 0 <= j < i -> a[j] <= !max }
if !max < a[i] then max := a[i]; if !max < a[i] then max := a[i];
sum := !sum + a[i] sum := !sum + a[i]
done; done;
...@@ -35,12 +34,11 @@ module MaxAndSum2 ...@@ -35,12 +34,11 @@ module MaxAndSum2
(l < h && exists k: int. l <= k < h && m = a[k])) (l < h && exists k: int. l <= k < h && m = a[k]))
let max_sum (a: array int) (n: int) = let max_sum (a: array int) (n: int) =
{ n >= 0 and length a = n and forall i:int. 0 <= i < n -> a[i] >= 0 } { 0 <= n = length a and forall i:int. 0 <= i < n -> a[i] >= 0 }
let s = ref 0 in let s = ref 0 in
let m = ref 0 in let m = ref 0 in
for i = 0 to n - 1 do for i = 0 to n - 1 do
invariant invariant { !s = sum a 0 i and is_max a 0 i !m and !s <= i * !m }
{ !s = sum a 0 i and is_max a 0 i !m and !s <= i * !m }
if !m < a[i] then m := a[i]; if !m < a[i] then m := a[i];
s := !s + a[i] s := !s + a[i]
done; done;
......
...@@ -106,14 +106,13 @@ Definition is_max(a:(array Z)) (l:Z) (h:Z) (m:Z): Prop := (forall (k:Z), ...@@ -106,14 +106,13 @@ Definition is_max(a:(array Z)) (l:Z) (h:Z) (m:Z): Prop := (forall (k:Z),
(m = (get1 a k)))). (m = (get1 a k)))).
Theorem WP_parameter_max_sum : forall (a:Z), forall (n:Z), forall (a1:(map Z Theorem WP_parameter_max_sum : forall (a:Z), forall (n:Z), forall (a1:(map Z
Z)), ((0%Z <= n)%Z /\ ((a = n) /\ forall (i:Z), ((0%Z <= i)%Z /\ Z)), ((((0%Z <= n)%Z /\ (n = a)) /\ (a = n)) /\ forall (i:Z),
(i < n)%Z) -> (0%Z <= (get a1 i))%Z)) -> ((0%Z <= (n - 1%Z)%Z)%Z -> ((0%Z <= i)%Z /\ (i < n)%Z) -> (0%Z <= (get a1 i))%Z) ->
forall (m:Z), forall (s:Z), forall (i:Z), ((0%Z <= i)%Z /\ ((0%Z <= (n - 1%Z)%Z)%Z -> forall (m:Z), forall (s:Z), forall (i:Z),
(i <= (n - 1%Z)%Z)%Z) -> (((s = (sum a1 0%Z i)) /\ ((is_max (mk_array a a1) ((0%Z <= i)%Z /\ (i <= (n - 1%Z)%Z)%Z) -> (((s = (sum a1 0%Z i)) /\
0%Z i m) /\ (s <= (i * m)%Z)%Z)) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> ((is_max (mk_array a a1) 0%Z i m) /\ (s <= (i * m)%Z)%Z)) ->
((m < (get a1 i))%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> forall (m1:Z), (((0%Z <= i)%Z /\ (i < a)%Z) -> ((~ (m < (get a1 i))%Z) ->
(m1 = (get a1 i)) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> forall (s1:Z), ((0%Z <= i)%Z /\ (i < a)%Z))))).
(s1 = (s + (get a1 i))%Z) -> (s1 <= ((i + 1%Z)%Z * m1)%Z)%Z)))))).
(* YOU MAY EDIT THE PROOF BELOW *) (* YOU MAY EDIT THE PROOF BELOW *)
intuition. intuition.
ring_simplify. ring_simplify.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter label : Type.
Parameter at1: forall (a:Type), a -> label -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition container := (map Z Z).
Parameter sum: (map Z Z) -> Z -> Z -> Z.
Axiom Sum_def_empty : forall (c:(map Z Z)) (i:Z) (j:Z), (j <= i)%Z -> ((sum c
i j) = 0%Z).
Axiom Sum_def_non_empty : forall (c:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((sum c i j) = ((get c i) + (sum c (i + 1%Z)%Z j))%Z).
Axiom Sum_right_extension : forall (c:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((sum c i j) = ((sum c i (j - 1%Z)%Z) + (get c (j - 1%Z)%Z))%Z).
Axiom Sum_transitivity : forall (c:(map Z Z)) (i:Z) (k:Z) (j:Z),
((i <= k)%Z /\ (k <= j)%Z) -> ((sum c i j) = ((sum c i k) + (sum c k
j))%Z).
Axiom Sum_eq : forall (c1:(map Z Z)) (c2:(map Z Z)) (i:Z) (j:Z),
(forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) -> ((get c1 k) = (get c2 k))) ->
((sum c1 i j) = (sum c2 i j)).
Definition sum1(a:(array Z)) (l:Z) (h:Z): Z := (sum (elts a) l h).
Definition is_max(a:(array Z)) (l:Z) (h:Z) (m:Z): Prop := (forall (k:Z),
((l <= k)%Z /\ (k < h)%Z) -> ((get1 a k) <= m)%Z) /\ (((h <= l)%Z /\
(m = 0%Z)) \/ ((l < h)%Z /\ exists k:Z, ((l <= k)%Z /\ (k < h)%Z) /\
(m = (get1 a k)))).
Theorem WP_parameter_max_sum : forall (a:Z), forall (n:Z), forall (a1:(map Z
Z)), ((((0%Z <= n)%Z /\ (n = a)) /\ (a = n)) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> (0%Z <= (get a1 i))%Z) ->
((0%Z <= (n - 1%Z)%Z)%Z -> forall (m:Z), forall (s:Z), forall (i:Z),
((0%Z <= i)%Z /\ (i <= (n - 1%Z)%Z)%Z) -> (((s = (sum a1 0%Z i)) /\
((is_max (mk_array a a1) 0%Z i m) /\ (s <= (i * m)%Z)%Z)) ->
(((0%Z <= i)%Z /\ (i < a)%Z) -> ((m < (get a1 i))%Z -> (((0%Z <= i)%Z /\
(i < a)%Z) -> forall (m1:Z), (m1 = (get a1 i)) -> (((0%Z <= i)%Z /\
(i < a)%Z) -> forall (s1:Z), (s1 = (s + (get a1 i))%Z) ->
(s1 <= ((i + 1%Z)%Z * m1)%Z)%Z)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter label : Type.
Parameter at1: forall (a:Type), a -> label -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition container := (map Z Z).
Parameter sum: (map Z Z) -> Z -> Z -> Z.
Axiom Sum_def_empty : forall (c:(map Z Z)) (i:Z) (j:Z), (j <= i)%Z -> ((sum c
i j) = 0%Z).
Axiom Sum_def_non_empty : forall (c:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((sum c i j) = ((get c i) + (sum c (i + 1%Z)%Z j))%Z).
Axiom Sum_right_extension : forall (c:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((sum c i j) = ((sum c i (j - 1%Z)%Z) + (get c (j - 1%Z)%Z))%Z).
Axiom Sum_transitivity : forall (c:(map Z Z)) (i:Z) (k:Z) (j:Z),
((i <= k)%Z /\ (k <= j)%Z) -> ((sum c i j) = ((sum c i k) + (sum c k
j))%Z).
Axiom Sum_eq : forall (c1:(map Z Z)) (c2:(map Z Z)) (i:Z) (j:Z),
(forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) -> ((get c1 k) = (get c2 k))) ->
((sum c1 i j) = (sum c2 i j)).
Definition sum1(a:(array Z)) (l:Z) (h:Z): Z := (sum (elts a) l h).
Definition is_max(a:(array Z)) (l:Z) (h:Z) (m:Z): Prop := (forall (k:Z),
((l <= k)%Z /\ (k < h)%Z) -> ((get1 a k) <= m)%Z) /\ (((h <= l)%Z /\
(m = 0%Z)) \/ ((l < h)%Z /\ exists k:Z, ((l <= k)%Z /\ (k < h)%Z) /\
(m = (get1 a k)))).
Theorem WP_parameter_max_sum : forall (a:Z), forall (n:Z), forall (a1:(map Z
Z)), (((0%Z <= n)%Z /\ (n = a)) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> (0%Z <= (get a1 i))%Z) -> ((0%Z <= (n - 1%Z)%Z)%Z ->
forall (m:Z), forall (s:Z), forall (i:Z), ((0%Z <= i)%Z /\
(i <= (n - 1%Z)%Z)%Z) -> (((s = (sum a1 0%Z i)) /\ ((is_max (mk_array a a1)
0%Z i m) /\ (s <= (i * m)%Z)%Z)) -> (((0%Z <= i)%Z /\ (i < a)%Z) ->
((m < (get a1 i))%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> forall (m1:Z),
(m1 = (get a1 i)) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> forall (s1:Z),
(s1 = (s + (get a1 i))%Z) -> (s1 <= ((i + 1%Z)%Z * m1)%Z)%Z)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
ring_simplify.
subst.
apply Zplus_le_compat_r.
apply Zle_trans with (i * m)%Z; auto.
auto with *.
Qed.
(* DO NOT EDIT BELOW *)
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