cleaning up example max_sum for the doc

parent fc7e0b73
......@@ -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_max_sum/
/examples/programs/vstte10_search_list/
/examples/programs/vstte10_aqueue/
/examples/programs/mergesort_list/
......
......@@ -928,7 +928,7 @@ DOC = api glossary ide intro library macros manpages \
DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX)
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
cd doc; $(RUBBER) -d manual.tex
# doc/manual.html: doc/manual.tex doc/version.tex
......
......@@ -187,3 +187,12 @@
pages = {223--228},
}
@Misc{vstte10comp,
author = {Natarajan Shankar and Peter Mueller},
title = {{Verified Software: Theories, Tools and Experiments
(VSTTE'10). Software Verification Competition}},
month = {August},
year = 2010,
address = {Edinburgh, Scotland},
note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}}
......@@ -8,9 +8,11 @@ Modules extend theories with \emph{programs}.
Programs can use all types, symbols, and constructs from the logic.
They also provide extra features:
\begin{itemize}
\item In a record type declaration, some fields can be declared
\item
In a record type declaration, some fields can be declared
\texttt{mutable}.
\item There are programming constructs with no counterpart in the logic:
\item
There are programming constructs with no counterpart in the logic:
\begin{itemize}
\item mutable field assignment;
\item sequence;
......@@ -19,15 +21,59 @@ They also provide extra features:
\item local and anonymous functions;
\item annotations: pre- and postconditions, assertions, loop invariants.
\end{itemize}
\item A program function can be non-terminating or can be proved
\item
A program function can be non-terminating or can be proved
to be terminating using a variant (a term together with a well-founded
order relation).
\item
An abstract program type $t$ can be introduced with a logical
\emph{model} $\tau$: inside programs, $t$ is abstract, and inside
annotations, $t$ is an alias for $\tau$.
\end{itemize}
% TODO: model types
%
Programs are contained in files with suffix \verb|.mlw|.
They are handled by the tool \texttt{why3ml}, which has a command line
similar to \texttt{why3}. For instance
\begin{verbatim}
% why3ml myfile.mlw
\end{verbatim}
will display the verification conditions extracted from modules in
file \texttt{myfile.mlw}, as a set of corresponding theories, and
\begin{verbatim}
% why3ml -P alt-ergo myfile.mlw
\end{verbatim}
will run the SMT solver Alt-Ergo on these verification conditions.
Program files are also handled by the GUI tool \texttt{why3ide}.
See Chapter~\ref{chap:manpages} for more details regarding command lines.
% files .mlw
% command line
% tutorial with examples: same fringe, max/sum
\medskip
As an introduction to \whyml, we use the five problems from the VSTTE
2010 verification competition~\cite{vstte10comp}.
\subsection{Problem 1: Sum and Maximum}
The first problem is stated as follows:
\begin{quote}
Given an $N$-element array of natural numbers,
write a program to compute the sum and the maximum of the
elements in the array.
\end{quote}
We assume $N \ge 0$ and $a[i] \ge 0$ for $0 \le i < N$, as precondition,
and we have to prove the following postcondition:
\begin{displaymath}
sum \le N \times max.
\end{displaymath}
\subsection{Problem 2: Inverting an Injection}
\subsection{Problem 3: Searching a Linked List}
\subsection{Problem 4: N-Queens}
\subsection{Problem 5: Amortized Queue}
% other examples: same fringe ?
%%% Local Variables:
%%% mode: latex
......
(* 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 sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
(((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a
i2))%Z.
Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
l u).
Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
Implicit Arguments map_eq_sub.
Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
(j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
Implicit Arguments exchange.
Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
(j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
(u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
Implicit Arguments permut_sub.
Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z
a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\
(r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2
i) = (get a1 j)).
Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
(j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Implicit Arguments exchange1.
Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
Implicit Arguments permut_sub1.
Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
(length a1)).
Implicit Arguments permut.
Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
Implicit Arguments array_eq_sub.
Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
Implicit Arguments array_eq.
Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)),
let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
Z)), let a4 := (mk_array a a3) in forall (i:Z), ((1%Z <= i)%Z /\
(i <= (a - 1%Z)%Z)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a4 a2)) ->
(((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a3 i) in
((((0%Z <= i)%Z /\ (i <= i)%Z) /\ ((permut (set1 a4 i result) a2) /\
((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
((~ (k1 = i)) -> ((~ (k2 = i)) -> ((get a3 k1) <= (get a3 k2))%Z))) /\
forall (k:Z), (((i + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a3
k))%Z))) -> forall (j:Z), forall (a5:(map Z Z)), let a6 := (mk_array a
a5) in ((((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut (set1 a6 j result) a2) /\
((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) ->
((~ (k1 = j)) -> ((~ (k2 = j)) -> ((get a5 k1) <= (get a5 k2))%Z))) /\
forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a5
k))%Z))) -> ((0%Z < j)%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\
((j - 1%Z)%Z < a)%Z) -> ((result < (get a5 (j - 1%Z)%Z))%Z ->
(((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> (((0%Z <= j)%Z /\
(j < a)%Z) -> forall (a7:(map Z Z)), let a8 := (mk_array a a7) in
((a7 = (set a5 j (get a5 (j - 1%Z)%Z))) -> ((exchange match (set1 a8
(j - 1%Z)%Z result) with
| mk_array _ elts1 => elts1
end match (set1 a6 j result) with
| mk_array _ elts1 => elts1
end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut (set1 a8
j1 result) a2))))))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
unfold set1.
unfold permut.
split.
simpl.
auto.
apply permut_trans with (elts (set1 (mk_array a a5) j (get a3 i))); auto.
subst j1.
apply permut_exchange with (j-1)%Z j.
simpl; omega.
simpl; omega.
assumption.
unfold permut in H17.
intuition.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 1: max and sum of an array *)
Problem 1: maximum and sum of an array *)
module M
module MaxAndSum
use import int.Int
use import module ref.Refint
use import module ref.Ref
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 }
let sum = ref 0 in
let max = ref 0 in
for i = 0 to n-1 do
invariant
for i = 0 to n - 1 do
invariant
{ !sum <= i * !max and forall j:int. 0 <= j < i -> a[j] <= !max }
if !max < a[i] then max := a[i];
sum += a[i]
sum := !sum + a[i]
done;
(!sum, !max)
{ let (sum, max) = result in sum <= n * max }
end
module MaxAndSum2
use import int.Int
use import module ref.Ref
use import module array.Array
use import module array.ArraySum
logic is_max (a: array int) (l h: int) (m: int) =
(forall k: int. l <= k < h -> a[k] <= m) &&
((h <= l && m = 0) ||
(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 }
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 }
if !m < a[i] then m := a[i];
s := !s + a[i]
done;
(!s, !m)
{ let (s, m) = result in s = sum a 0 n and is_max a 0 n m and s <= n * m }
end
module TestCase
use import module MaxAndSum2
use import module array.Array
use import module array.ArraySum
let test_case () =
let n = 10 in
let a = make n 0 in
a[0] <- 9;
a[1] <- 5;
a[2] <- 0;
a[3] <- 2;
a[4] <- 7;
a[5] <- 3;
a[6] <- 2;
a[7] <- 1;
a[8] <- 10;
a[9] <- 6;
let (s, m) = max_sum a n in
assert { s = 45 };
assert { m = 10 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_max_sum.gui"
......
(* 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 /\ ((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.
ring_simplify.
subst.
apply Zplus_le_compat_r.
apply Zle_trans with (i * m)%Z; auto.
auto with *.
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.
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 (max:Z), forall (sum:Z), forall (i:Z), ((0%Z <= i)%Z /\
(i <= (n - 1%Z)%Z)%Z) -> (((sum <= (i * max)%Z)%Z /\ forall (j:Z),
((0%Z <= j)%Z /\ (j < i)%Z) -> ((get a1 j) <= max)%Z) -> (((0%Z <= i)%Z /\
(i < a)%Z) -> ((max < (get a1 i))%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) ->
forall (max1:Z), (max1 = (get a1 i)) -> (((0%Z <= i)%Z /\ (i < a)%Z) ->
forall (sum1:Z), (sum1 = (sum + (get a1 i))%Z) ->
(sum1 <= ((i + 1%Z)%Z * max1)%Z)%Z)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
ring_simplify.
subst.
apply Zplus_le_compat_r.
apply Zle_trans with (i * max)%Z; auto.
auto with *.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
......@@ -17,10 +17,10 @@ module Array
logic ([]) (a: array 'a) (i: int) : 'a = get a i
logic ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
parameter ([]) (a:array 'a) (i:int) :
parameter ([]) (a: array 'a) (i: int) :
{ 0 <= i < length a } 'a reads a { result = a[i] }
parameter ([]<-) (a:array 'a) (i:int) (v:'a) :
parameter ([]<-) (a: array 'a) (i: int) (v: 'a) :
{ 0 <= i < length a } unit writes a { a.elts = M.set (old a.elts) i v }
parameter length (a: array 'a) : {} int { result = a.length }
......@@ -28,7 +28,7 @@ module Array
(* unsafe get/set operations with no precondition *)
exception OutOfBounds