New example: fenwick trees

examples/fenwick.mlw

+
+(* Fenwick trees (or binary indexed tree) for prefix/interval sums.
+   Represent an integer array over interval [0;n[ such that the following
+   operations are both efficient:
+   . incrementation of individual cell (O(log(n)))
+   . Query sum of elements over interval [a;b[ (O(log(b-a)))
+
+   Author: Martin Clochard (Université Paris Sud) *)
+
+(* Array-based implementation with i->(2i+1,2i+2) node encoding:
+   . Integer represent nodes
+   . 0 is the root
+   . childs of node n are 2n+1 and 2n+2
+   . Leaves represent the model array cells. For n > 0 elements in the model,
+     they are represented by the cells over the range [n-1;2n-1[
+   The structure manage queries by keeping for each node the sum of the
+   values of all descendant leaves, which we call here 'node summary' *)
+module Fenwick
+
+  use import int.Int
+  use import int.ComputerDivision
+  use import ref.Ref
+  use import int.Sum
+  use import array.Array as A
+
+  (* Encode fenwick trees within an array. The leaves field represent
+     the actual number of element within the model. *)
+  type fenwick = {
+    t : array int;
+    ghost leaves : int;
+  }
+
+  (* Invariant *)
+  predicate valid (f:fenwick) =
+    f.leaves >= 0 /\
+    f.t.length = (if f.leaves = 0 then 0 else 2 * f.leaves - 1) /\
+    forall i. 0 <= i /\ i < f.leaves - 1 ->
+      f.t[i] = f.t[2*i+1] + f.t[2*i+2]
+
+  (* Get the i-th elements of the model. *)
+  function get (f:fenwick) (i:int) : int = f.t[i+f.leaves-1]
+  (* Get the sum of elements over range [a;b[ *)
+  function rget (f:fenwick) (a b:int) : int = sum a b (get f)
+
+  (* Create a Fenwick tree initialized at 0 *)
+  let make (lv:int) : fenwick
+    requires { lv >= 0 }
+    ensures { valid result }
+    ensures { forall i. 0 <= i < lv -> get result i = 0 }
+    ensures { result.leaves = lv }
+  = { t = if lv = 0 then make 0 0 else make (2*lv-1) 0;
+      leaves = lv }
+
+  (* Add x to the l-th cell *)
+  let add (f:fenwick) (l:int) (x:int) : unit
+    requires { 0 <= l < f.leaves /\ valid f }
+    ensures { valid f }
+    ensures { forall i. 0 <= i < f.leaves /\ i <> l ->
+      get f i = get (old f) i }
+    ensures { get f l = get (old f) l + x }
+  = let lc = ref (div f.t.length 2 + l) in
+    f.t[!lc] <- f.t[!lc] + x;
+    (* Update node summaries for all elements on the path
+       from the updated leaf to the root. *)
+    'I:
+    while !lc <> 0 do
+      invariant { 0 <= !lc < f.t.length }
+      invariant { forall i. 0 <= i /\ i < f.leaves - 1 ->
+        f.t[i] = f.t[2*i+1] + f.t[2*i+2] -
+          if 2*i+1 <= !lc <= 2*i+2 then x else 0 }
+      invariant { forall i. f.leaves - 1 <= i < f.t.length ->
+        f.t[i] = (at f 'I).t[i] }
+      variant { !lc }
+      lc := div (!lc - 1) 2;
+      f.t[!lc] <- f.t[!lc] + x
+    done
+
+  (* Lemma to shift dum indices. *)
+  let rec ghost sum_dec (a b c:int) : unit
+    requires { a <= b }
+    ensures { forall f g. (forall i. a <= i < b -> f i = g (i+c)) ->
+      sum a b f = sum (a+c) (b+c) g }
+    variant { b - a }
+  = if a < b then sum_dec (a+1) b c
+
+  (* Crucial lemma for the query routine: Summing the node summaries
+     over range [2a+1;2b+1[ is equivalent to summing node summaries
+     over range [a;b[. This is because the elements of range [2a+1;2b+1[
+     are exactly the childs of elements of range [a;b[. *)
+  let rec ghost fen_compact (f:fenwick) (a b:int) : unit
+    requires { 0 <= a <= b /\ 2 * b < f.t.length /\ valid f }
+    ensures { sum a b (A.get f.t) = sum (2*a+1) (2*b+1) (A.get f.t) }
+    variant { b - a }
+  = if a < b then fen_compact f (a+1) b
+
+  (* Query sum of elements over interval [a,b[. *)
+  let query (f:fenwick) (a b:int) : int
+    requires { 0 <= a <= b <= f.leaves /\ valid f }
+    ensures { result = rget f a b }
+  = let lv = div f.t.length 2 in
+    let ra = ref (a + lv) in let rb = ref (b + lv) in
+    let acc = ref 0 in
+    ghost sum_dec a b lv;
+    (* If ra = rb, the sum is 0.
+       Otherwise, adjust the range to odd boundaries in constant time
+       and use compaction lemma to halve interval size. *)
+    while !ra <> !rb do
+      invariant { 0 <= !ra <= !rb <= f.t.length }
+      invariant { !acc + sum !ra !rb (A.get f.t) = rget f a b }
+      variant { !rb - !ra }
+      if mod !ra 2 = 0 then acc := !acc + f.t[!ra];
+      ra := div !ra 2;
+      rb := !rb - 1;
+      if mod !rb 2 <> 0 then acc := !acc + f.t[!rb];
+      rb := div !rb 2;
+      ghost fen_compact f !ra !rb
+    done;
+    !acc
+
+end

examples/fenwick/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<file name="../fenwick.mlw">
+<theory name="Fenwick" sum="2acffcabae53480cd6db25628871c757">
+ <goal name="WP_parameter make" expl="VC for make">
+ <proof prover="1"><result status="valid" time="0.03" steps="29"/></proof>
+ </goal>
+ <goal name="WP_parameter add" expl="VC for add">
+ <proof prover="1"><result status="valid" time="0.74" steps="353"/></proof>
+ </goal>
+ <goal name="WP_parameter sum_dec" expl="VC for sum_dec">
+ <proof prover="1"><result status="valid" time="0.06" steps="67"/></proof>
+ </goal>
+ <goal name="WP_parameter fen_compact" expl="VC for fen_compact">
+ <proof prover="0"><result status="valid" time="1.36"/></proof>
+ </goal>
+ <goal name="WP_parameter query" expl="VC for query">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter query.1" expl="1. precondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+  </goal>
+  <goal name="WP_parameter query.2" expl="2. loop invariant init">
+  <proof prover="1"><result status="valid" time="0.02" steps="16"/></proof>
+  </goal>
+  <goal name="WP_parameter query.3" expl="3. loop invariant init">
+  <proof prover="1"><result status="valid" time="0.19" steps="154"/></proof>
+  </goal>
+  <goal name="WP_parameter query.4" expl="4. index in array bounds">
+  <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+  </goal>
+  <goal name="WP_parameter query.5" expl="5. index in array bounds">
+  <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
+  </goal>
+  <goal name="WP_parameter query.6" expl="6. precondition">
+  <proof prover="1"><result status="valid" time="0.13" steps="95"/></proof>
+  </goal>
+  <goal name="WP_parameter query.7" expl="7. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="25"/></proof>
+  </goal>
+  <goal name="WP_parameter query.8" expl="8. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.78" steps="434"/></proof>
+  </goal>
+  <goal name="WP_parameter query.9" expl="9. loop variant decrease">
+  <proof prover="1"><result status="valid" time="0.11" steps="74"/></proof>
+  </goal>
+  <goal name="WP_parameter query.10" expl="10. precondition">
+  <proof prover="1"><result status="valid" time="0.08" steps="69"/></proof>
+  </goal>
+  <goal name="WP_parameter query.11" expl="11. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
+  </goal>
+  <goal name="WP_parameter query.12" expl="12. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="1.57" steps="646"/></proof>
+  </goal>
+  <goal name="WP_parameter query.13" expl="13. loop variant decrease">
+  <proof prover="1"><result status="valid" time="0.02" steps="32"/></proof>
+  </goal>
+  <goal name="WP_parameter query.14" expl="14. index in array bounds">
+  <proof prover="1"><result status="valid" time="0.00" steps="15"/></proof>
+  </goal>
+  <goal name="WP_parameter query.15" expl="15. precondition">
+  <proof prover="1"><result status="valid" time="0.14" steps="97"/></proof>
+  </goal>
+  <goal name="WP_parameter query.16" expl="16. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+  </goal>
+  <goal name="WP_parameter query.17" expl="17. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.88" steps="427"/></proof>
+  </goal>
+  <goal name="WP_parameter query.18" expl="18. loop variant decrease">
+  <proof prover="1"><result status="valid" time="0.14" steps="70"/></proof>
+  </goal>
+  <goal name="WP_parameter query.19" expl="19. precondition">
+  <proof prover="1"><result status="valid" time="0.09" steps="73"/></proof>
+  </goal>
+  <goal name="WP_parameter query.20" expl="20. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+  </goal>
+  <goal name="WP_parameter query.21" expl="21. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="1.00" steps="546"/></proof>
+  </goal>
+  <goal name="WP_parameter query.22" expl="22. loop variant decrease">
+  <proof prover="1"><result status="valid" time="0.05" steps="55"/></proof>
+  </goal>
+  <goal name="WP_parameter query.23" expl="23. postcondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>