Commit 7b1fdd68 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Example sumrange completed using interactive proofs.

However, it remains to specify and prove that [query] in cumulative tree is logarithmic
parent 98e4eca4
(** {1 Range Sum Queries}
We are interested in specifying and proving correct
data structures that support efficient computation of the sum of the
values over an arbitrary range of an array.
Concretely, given an array of integers [a], and given a range
delimited by indices [i] (inclusive) and [j] (exclusive), we wish
to compute the value: [\sum_{k=i}^{j-1} a[k]].
In the first part, we consider a simple loop
for computing the sum in linear time.
In the second part, we introduce a cumulative sum array
that allows answering arbitrary range queries in constant time.
In the third part, we explore a tree data structure that
supports modification of values from the underlying array [a],
with logarithmic time operations.
*)
(** {2 Specification of Range Sum} *)
module ArraySum
use export int.Int
use export array.Array
(** [sum a i j] denotes the sum [\sum_{i <= k < j} a[k]].
It is axiomatizated by the two following axioms expressing
the recursive definition
if [i <= j] then [sum a i j = 0]
if [i < j] then [sum a i j = a[i] + sum a (i+1) j]
*)
function sum (array int) int int : int
(** [sum a i j] denotes the sum Sum_{i <= k < j} a[k] *)
axiom sum_def_empty :
forall a : array int, i j : int. j <= i -> sum a i j = 0
......@@ -15,12 +46,11 @@ module ArraySum
forall a: array int, i j : int. i < j /\ 0 <= i < a.length ->
sum a i j = a[i] + sum a (i+1) j
(*
lemma sum_right_aux : forall a x j.
0 < j <= a.length -> 0 < x <= j ->
sum a (j-x) j = sum a (j-x) (j-1) + a [j-1]
*)
(** lemma for summation from the right:
if [i < j] then [sum a i j = sum a i (j-1) + a[j-1]]
*)
lemma sum_right : forall a : array int, i j : int.
0 <= i < j <= a.length ->
sum a i j = sum a i (j-1) + a[j-1]
......@@ -29,6 +59,9 @@ end
(** {2 First algorithm, a linear one} *)
module Simple
use import ArraySum
......@@ -49,10 +82,58 @@ module Simple
end
(** {2 Additional lemmas on [sum]}
needed in the remaining code *)
module ExtraLemmas
use array.Array
use import ArraySum
(** summation in adjacent intervals *)
lemma sum_concat : forall a:array int, i j k:int.
0 <= i <= j <= k <= a.length ->
sum a i k = sum a i j + sum a j k
(** Frame lemma for [sum], that is [sum a i j] depends only
of values of [a[i..j-1]] *)
lemma sum_frame : forall a1 a2 : array int, i j : int.
0 <= i <= j ->
j <= a1.length ->
j <= a2.length ->
(forall k : int. i <= k < j -> a1[k] = a2[k]) ->
sum a1 i j = sum a2 i j
(** Updated lemma for [sum]: how does [sum a i j] changes when
[a[k]] is changed for some [k] in [[i..j-1]] *)
lemma sum_update : forall a:array int, i v l h:int.
0 <= l <= i < h <= a.length ->
sum (a[i<-v]) l h = sum a l h + v - a[i]
end
(** {2 Algorithm 2: using a cumulative array}
creation of cumulative array is linear
query is in constant time
array update is linear
*)
module CumulativeArray
use array.Array
use import ArraySum
use ExtraLemmas
predicate is_cumulative_array_for (c:array int) (a:array int) =
c.length = a.length + 1 /\
......@@ -69,11 +150,6 @@ module CumulativeArray
done;
s
lemma sum_concat : forall a:array int, i j k:int.
0 <= i <= j <= k <= a.length ->
sum a i k = sum a i j + sum a j k
(** [query c i j a] returns the sum of elements in [a] between
index [i] inclusive and index [j] exclusive, in constant time *)
let query (c:array int) (i j:int) (ghost a:array int): int
......@@ -81,34 +157,19 @@ module CumulativeArray
requires { 0 <= i <= j < c.length }
ensures { result = sum a i j }
= c[j] - c[i]
lemma sum_frame : forall a1 a2 : array int, i j : int.
0 <= i <= j ->
j <= a1.length ->
j <= a2.length ->
(forall k : int. i <= k < j -> a1[k] = a2[k]) ->
sum a1 i j = sum a2 i j
let rec lemma sum_update (a:array int) (i v l h:int) : unit
requires { 0 <= l <= i < h <= a.length }
variant { h }
ensures { sum (a[i<-v]) l h = sum a l h + v - a[i] }
= if h > i + 1 then sum_update a i v l (h-1)
(*>*)
(** [update c i v a] updates cell [a[i]] to value [v] and updates
the cumulative array [c] accordingly *)
let update (c:array int) (i:int) (v:int) (ghost a:array int) : unit
requires { (*<a*) is_cumulative_array_for c a (*>*) } (*<e*)
requires { 0 <= i < a.length } (*>*)
writes { (*<u*) c, a (*>*) }
requires { is_cumulative_array_for c a }
requires { 0 <= i < a.length }
writes { c, a }
ensures { is_cumulative_array_for c a }
ensures { a[i] = v }
ensures { forall k. 0 <= k < a.length /\ k <> i ->
a[k] = (old a)[k] }
= (*<c*) 'Init:
= 'Init:
let incr = v - c[i+1] + c[i] in
a[i] <- v;
for j=i+1 to c.length-1 do
......@@ -116,7 +177,6 @@ module CumulativeArray
invariant { forall k. 0 <= k < j -> c[k] = sum a 0 k }
c[j] <- c[j] + incr
done
(*>*)
end
......@@ -125,10 +185,24 @@ end
(** {2 Algorithm 3: using a cumulative tree}
creation is linear
query is logarithmic
update is logarithmic
*)
module CumulativeTree
use array.Array
use import ArraySum
use ExtraLemmas
use import int.ComputerDivision
type indexes =
......@@ -145,77 +219,62 @@ module CumulativeTree
| Node ind _ _ -> ind
end
(* QUESTION 11 *)
(*<e*)
predicate is_indexes_for (ind:indexes) (a:array int) (i j:int) =
ind.low = i /\ ind.high = j /\
0 <= i < j <= a.length /\
ind.isum = sum a i j
(*>*)
predicate is_tree_for (t:tree) (a:array int) (i j:int) =
match t with
| Leaf ind ->
(*<a*) is_indexes_for ind a i j /\ j = i+1 (*>*)
is_indexes_for ind a i j /\ j = i+1
| Node ind l r ->
(*<a*) is_indexes_for ind a i j /\
is_indexes_for ind a i j /\
i = l.indexes.low /\ j = r.indexes.high /\
let m = l.indexes.high in
m = r.indexes.low /\
i < m < j /\ m = div (i+j) 2 /\
is_tree_for l a i m /\
is_tree_for r a m j (*>*)
is_tree_for r a m j
end
(* QUESTION 12 *)
(*<e*)
let rec lemma sum_concat (a:array int) (i j k:int) : unit
requires { 0 <= i <= j <= k <= a.length }
variant { j - i }
ensures { sum a i k = sum a i j + sum a j k }
= if i < j then sum_concat a (i+1) j k
(*>*)
(** {3 creation of cumulative tree} *)
let rec tree_of_array (a:array int) (i j:int) : tree
requires { (*<a*) 0 <= i < j <= a.length (*>*) }
variant { (*<v*) j - i (*>*) }
ensures { (*<a*) is_tree_for result a i j (*>*) }
requires { 0 <= i < j <= a.length }
variant { j - i }
ensures { is_tree_for result a i j }
= if i+1=j then begin
(*<c*) Leaf { low = i; high = j; isum = a[i] } (*>*)
Leaf { low = i; high = j; isum = a[i] }
end
else
begin
let m = div (i+j) 2 in
(*<c*)
assert { i < m < j };
let l = tree_of_array a i m in
let r = tree_of_array a m j in
let s = l.indexes.isum + r.indexes.isum in
assert { s = sum a i j };
Node { low = i; high = j; isum = s} l r
(*>*)
end
(* QUESTION 13 *)
let create (a:array int) : tree
requires { (*<a*) a.length >= 1 (*>*) }
requires { a.length >= 1 }
ensures { is_tree_for result a 0 a.length }
= (*<c*) tree_of_array a 0 a.length (*>*)
= tree_of_array a 0 a.length
(** {3 query using cumulative tree} *)
(* QUESTION 14 *)
let rec query_aux (t:tree) (ghost a: array int)
(i j:int) : int
requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
requires { (*<a*) 0 <= t.indexes.low <= i < j <= t.indexes.high <= a.length (*>*) }
variant { (*<v*) t (*>*) }
ensures { (*<a*) result = sum a i j (*>*) }
= (*<c*)
match t with
requires { is_tree_for t a t.indexes.low t.indexes.high }
requires { 0 <= t.indexes.low <= i < j <= t.indexes.high <= a.length }
variant { t }
ensures { result = sum a i j }
= match t with
| Leaf ind ->
ind.isum
| Node ind l r ->
......@@ -223,105 +282,39 @@ module CumulativeTree
let k3 = ind.high in
if i=k1 && j=k3 then ind.isum else
let m = l.indexes.high in
if j <= m then query_aux l a (*k1 m*) i j else
if i >= m then query_aux r a (*m k3*) i j else
query_aux l a (*k1 m*) i m + query_aux r a (*m k3*) m j
if j <= m then query_aux l a i j else
if i >= m then query_aux r a i j else
query_aux l a i m + query_aux r a m j
end
(*>*)
(* QUESTION 16 *)
let query (t:tree) (ghost a: array int) (i j:int) : int
requires { 0 <= i <= j <= a.length }
requires { (*<a*) is_tree_for t a 0 a.length (*>*) }
requires { is_tree_for t a 0 a.length }
ensures { result = sum a i j }
= (*<c*) if i=j then 0 else query_aux t a (*0 a.length*) i j (*>*)
(*<e*) (* version arthur *)
= if i=j then 0 else query_aux t a i j
predicate is_disjoint (ind:indexes) (i j:int) =
(j <= ind.low) || (i >= ind.high)
predicate is_fully_covered (ind:indexes) (i j:int) =
i <= ind.low && ind.high <= j
(** frame lemma for predicate [is_tree_for] *)
lemma is_tree_for_frame : forall t:tree, a:array int, k v i j:int.
0 <= k < a.length ->
k < i \/ k >= j ->
is_tree_for t a i j ->
is_tree_for t a[k<-v] i j
use import int.MinMax
(** {3 update cumulative tree} *)
let rec query2 (t:tree) (ghost a: array int)
(i j:int) : int
requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
(* requires { (*<a*) 0 <= t.indexes.low <= i /\ j <= t.indexes.high <= a.length (*>*) } *)
variant { (*<v*) t (*>*) }
ensures { (*<a*) result = sum a (max t.indexes.low i) (min t.indexes.high j) (*>*) }
= let ind = indexes t in
if is_disjoint ind i j then 0
else if is_fully_covered ind i j then ind.isum
else
match t with
| Leaf _ -> absurd
(* car on a forcément is_disjoint ou bien is_fully_covered *)
| Node _ l r ->
query2 l a i j + query2 r a i j
(* utiliser un lemme de découpage des intersections *)
end
let query3 (t:tree) (ghost a: array int) (i j:int) : int
requires { 0 <= i <= j <= a.length }
requires { (*<a*) is_tree_for t a 0 a.length (*>*) }
ensures { result = sum a i j }
= (*<c*) query2 t a i j (*>*)
(*>*)
(* QUESTIONS 17 and 18 *)
(*<e*)
let rec lemma is_tree_for_frame (t:tree) (a:array int) (k v i j:int)
requires { 0 <= k < a.length }
requires { k < i \/ k >= j }
requires { is_tree_for t a i j }
variant { t }
ensures { is_tree_for t a[k<-v] i j }
= match t with
| Leaf _ -> ()
| Node _ l r ->
is_tree_for_frame l a k v i l.indexes.high;
is_tree_for_frame r a k v l.indexes.high j;
end
let rec lemma sum_right (a : array int) (i j : int)
requires { 0 <= i < j <= a.length }
variant { j - i }
ensures { sum a i j = sum a i (j-1) + a[j-1] }
= if i < j-1 then sum_right a (i+1) j
let rec lemma sum_frame (a1 a2 : array int) (i j : int) : unit
requires { 0 <= i <= j }
requires { j <= a1.length }
requires { j <= a2.length }
requires { forall k : int. i <= k < j -> a1[k] = a2[k] }
variant { j - i }
ensures { sum a1 i j = sum a2 i j }
= if i < j then sum_frame a1 a2 (i+1) j
let rec lemma sum_update (a:array int) (i v l h:int) : unit
requires { 0 <= l <= i < h <= a.length }
variant { h }
ensures { sum (a[i<-v]) l h = sum a l h + v - a[i] }
= if h > i + 1 then sum_update a i v l (h-1)
(*>*)
let rec update_aux (t:tree) (i:int) (ghost a :array int) (v:int) : (tree,int)
requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
(*<e*) requires { t.indexes.low <= i < t.indexes.high }
variant { t } (*>*)
requires { is_tree_for t a t.indexes.low t.indexes.high }
requires { t.indexes.low <= i < t.indexes.high }
variant { t }
returns { (t',delta) ->
(*<a*) delta = v - a[i] /\
delta = v - a[i] /\
t'.indexes.low = t.indexes.low /\
t'.indexes.high = t.indexes.high /\
is_tree_for t' a[i<-v] t'.indexes.low t'.indexes.high (*>*) }
= (*<c*) match t with
is_tree_for t' a[i<-v] t'.indexes.low t'.indexes.high }
= match t with
| Leaf ind ->
assert { i = ind.low };
(Leaf { ind with isum = v }, v - ind.isum)
......@@ -337,23 +330,32 @@ let rec query2 (t:tree) (ghost a: array int)
assert { is_tree_for l a[i<-v] t.indexes.low m };
assert { is_tree_for r' a[i<-v] m t.indexes.high };
(Node {ind with isum = ind.isum + delta} l r',delta)
end(*>*)
(* QUESTION 19 *)
end
let update (t:tree) (ghost a:array int) (i v:int) : tree
requires { (*<a*) 0 <= i < a.length (*>*) } (*<e*)
requires { is_tree_for t a 0 a.length } (*>*)
requires { 0 <= i < a.length }
requires { is_tree_for t a 0 a.length }
writes { a }
ensures { a[i] = v }
ensures { forall k. 0 <= k < a.length /\ k <> i -> a[k] = (old a)[k] }
ensures { is_tree_for result a 0 a.length }
= let t,_ = (*<c*) update_aux t i a v (*>*) in
= let t,_ = update_aux t i a v in
a[i] <- v;
t
(* complexity *)
(** {2 complexity analysis}
We would like to prove that [query] is really logarithmic. This is
non-trivial because there are two recursive calls in some cases.
So far, we are only able to prove that [update] is logarithmic
We express the complexity by passing a ``credit'' as a ghost
parameter. We pose the precondition that the credit is at least
equal to the depth of the tree.
*)
use import int.MinMax
......@@ -366,23 +368,22 @@ let rec query2 (t:tree) (ghost a: array int)
use import ref.Ref
let rec update_compl (t:tree) (i:int) (ghost a :array int) (v:int) (ghost c:ref int): (tree,int)
requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
(*<e*) requires { t.indexes.low <= i < t.indexes.high }
requires { is_tree_for t a t.indexes.low t.indexes.high }
requires { t.indexes.low <= i < t.indexes.high }
requires { !c >= depth t }
variant { t } (*>*)
variant { t }
returns { (t',delta) ->
(*<a*) delta = v - a[i] /\
delta = v - a[i] /\
t'.indexes.low = t.indexes.low /\
t'.indexes.high = t.indexes.high /\
is_tree_for t' a[i<-v] t'.indexes.low t'.indexes.high (*>*) }
is_tree_for t' a[i<-v] t'.indexes.low t'.indexes.high }
= c := !c - 1;
match t with
| Leaf ind ->
(*<c*) assert { i = ind.low };
(Leaf { ind with isum = v }, v - ind.isum)
(*>*)
assert { i = ind.low };
(Leaf { ind with isum = v }, v - ind.isum)
| Node ind l r ->
(*<c*) let m = l.indexes.high in
let m = l.indexes.high in
if i < m then
let l',delta = update_compl l i a v c in
assert { is_tree_for l' a[i<-v] t.indexes.low m };
......@@ -395,6 +396,9 @@ let rec query2 (t:tree) (ghost a: array int)
(Node {ind with isum = ind.isum + delta} l r',delta) (*>*)
end
(** auxiliary result: depth of a cumulative tree is indeed
logarithmic in function of the number of its elements *)
use import bv.Pow2int
let rec lemma depth_is_log (t:tree) (a :array int) (k:int)
......
......@@ -3,26 +3,27 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../sumrange.mlw">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../sumrange.mlw" proved="true">
<theory name="ArraySum" proved="true" sum="c43abcc65051af09a54f471f27f69208">
<goal name="sum_right" proved="true">
<transf name="assert" proved="true" arg1="(forall x. 0 &lt; x &lt; j -&gt; sum a (j-x) j = sum a (j-x) (j-1) + a[j-1])">
<goal name="sum_right.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_right.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sum_right.0.1" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="sum_right.1" proved="true">
<transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
<goal name="sum_right.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
......@@ -32,107 +33,248 @@
<theory name="Simple" proved="true" sum="17809040d6493313e8bff554cd196ef3">
<goal name="WP_parameter query" expl="VC for query" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter query.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter query.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter query.2" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter query.3" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter query.4" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="CumulativeArray" proved="true" sum="26b3e456f7b133ab67010bf9177097cd">
<goal name="WP_parameter create" expl="VC for create" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<theory name="ExtraLemmas" proved="true" sum="06d9ed7291283643f4ece6e481eb7dd6">
<goal name="sum_concat" proved="true">
<transf name="induction" proved="true" arg1="k">
<goal name="sum_concat.0" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_concat.1" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter query" expl="VC for query" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sum_frame" proved="true">
<transf name="assert" proved="true" arg1="(forall x. 0 &lt;= x &lt;= j-i -&gt; sum a1 (j-x) j = sum a2 (j-x) j)">
<goal name="sum_frame.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_frame.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_frame.0.1" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="sum_frame.1" proved="true">
<transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
<goal name="sum_frame.1.0" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter sum_update" expl="VC for sum_update" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter update" expl="VC for update" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<goal name="sum_update" proved="true">
<transf name="induction" proved="true" arg1="h" arg2="from" arg3="i+1">
<goal name="sum_update.0" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.0.0" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
</transf>