From 361252b424117ee9c6fbe8da5946b6531b3d28de Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Tue, 21 Jun 2011 12:50:41 +0200 Subject: [PATCH] documentation: solution for VSTTE'10 problem 1 --- doc/whyml.tex | 161 ++++++++++++++++++ examples/programs/vstte10_max_sum.mlw | 10 +- ...um.mlw_MaxAndSum2_WP_parameter max_sum_1.v | 15 +- ...um.mlw_MaxAndSum2_WP_parameter max_sum_2.v | 124 ++++++++++++++ ...um.mlw_MaxAndSum2_WP_parameter max_sum_3.v | 127 ++++++++++++++ .../programs/vstte10_max_sum/why3session.xml | 106 ++++++------ 6 files changed, 471 insertions(+), 72 deletions(-) create mode 100644 examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_2.v create mode 100644 examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_3.v diff --git a/doc/whyml.tex b/doc/whyml.tex index 3ec235164..6a23a643c 100644 --- a/doc/whyml.tex +++ b/doc/whyml.tex @@ -63,16 +63,177 @@ and we have to prove the following postcondition: \begin{displaymath} sum \le N \times max. \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} +\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} +\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} +\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} +\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 ? %%% Local Variables: diff --git a/examples/programs/vstte10_max_sum.mlw b/examples/programs/vstte10_max_sum.mlw index ac35d224f..b01507c87 100644 --- a/examples/programs/vstte10_max_sum.mlw +++ b/examples/programs/vstte10_max_sum.mlw @@ -8,12 +8,11 @@ module MaxAndSum use import module array.Array 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 max = ref 0 in for i = 0 to n - 1 do - invariant - { !sum <= i * !max and forall j:int. 0 <= j < i -> a[j] <= !max } + invariant { !sum <= i * !max } if !max < a[i] then max := a[i]; sum := !sum + a[i] done; @@ -35,12 +34,11 @@ module MaxAndSum2 (l < h && exists k: int. l <= k < h && m = a[k])) 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 m = ref 0 in for i = 0 to n - 1 do - invariant - { !s = sum a 0 i and is_max a 0 i !m and !s <= i * !m } + invariant { !s = sum a 0 i and is_max a 0 i !m and !s <= i * !m } if !m < a[i] then m := a[i]; s := !s + a[i] done; diff --git a/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_1.v b/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_1.v index 4485ca7bc..dbd0c90bb 100644 --- a/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_1.v +++ b/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_1.v @@ -106,14 +106,13 @@ Definition is_max(a:(array Z)) (l:Z) (h:Z) (m:Z): Prop := (forall (k: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 /\ ((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)))))). + 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))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. ring_simplify. diff --git a/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_2.v b/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_2.v new file mode 100644 index 000000000..f13824e89 --- /dev/null +++ b/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_2.v @@ -0,0 +1,124 @@ +(* 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 *) + + diff --git a/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_3.v b/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_3.v new file mode 100644 index 000000000..7da3ff3e2 --- /dev/null +++ b/examples/programs/vstte10_max_sum/vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_3.v @@ -0,0 +1,127 @@ +(* 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 *) + + diff --git a/examples/programs/vstte10_max_sum/why3session.xml b/examples/programs/vstte10_max_sum/why3session.xml index 185729977..dba89eea8 100644 --- a/examples/programs/vstte10_max_sum/why3session.xml +++ b/examples/programs/vstte10_max_sum/why3session.xml @@ -3,63 +3,53 @@ - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - + - + - + - + - + @@ -68,73 +58,73 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + + + - - - + + + - - - + + + - + - + - + - + @@ -143,7 +133,7 @@ - + @@ -195,12 +185,12 @@ - + - + @@ -208,9 +198,9 @@ - + - + -- GitLab