Wiki Agenda Contact Version française

Sparse Arrays in Why3

This is a Why3 version of the Sparse Arrays example, the first example of the VACID-0 benchmarks


Authors: Jean-Christophe Filliâtre / Andrei Paskevich

Topics: Array Data Structure / Data Structures / Permutation

Tools: Why3

References: The VACID-0 Benchmarks / The VerifyThis Benchmarks

See also: Sparse Arrays in Capucine

see also the index (by topic, by tool, by reference, by year)


module SparseArray

(*
      If the sparse array contains three elements x y z, at index
      a b c respectively, then the three arrays look like this:

              b     a      c
values +-----+-+---+-+----+-+----+
       |     |y|   |x|    |z|    |
       +-----+-+---+-+----+-+----+

index  +-----+-+---+-+----+-+----+
       |     |1|   |0|    |2|    |
       +-----+-+---+-+----+-+----+

        0 1 2  n=3
back   +-+-+-+-------------------+
       |a|b|c|                   |
       +-+-+-+-------------------+

*)

  use import int.Int
  use import array.Array as A

  constant maxlen : int = 1000

  type sparse_array 'a = { values : array 'a;
                           index  : array int;
                           back   : array int;
                   mutable card   : int;
                           def    : 'a; }
  invariant {
    0 <= self.card <= A.length self.values <= maxlen /\
    A.length self.values = A.length self.index = A.length self.back /\
    forall i : int.
      0 <= i < self.card ->
      0 <= self.back[i] < A.length self.values /\ self.index[self.back[i]] = i
  }

  predicate is_elt (a: sparse_array 'a) (i: int) =
    0 <= a.index[i] < a.card /\ a.back[a.index[i]] = i

  function value (a: sparse_array 'a) (i: int) : 'a =
    if is_elt a i then
      a.values[i]
    else
      a.def

  function length (a: sparse_array 'a) : int = A.length a.values

  (* creation *)

  val malloc (n:int) : array 'a ensures { A.length result = n }

  let create (sz: int) (d: 'a)
    requires { 0 <= sz <= maxlen }
    ensures { result.card = 0 /\ result.def = d /\ length result = sz }
  = { values = malloc sz;
      index  = malloc sz;
      back   = malloc sz;
      card   = 0;
      def    = d }

  (* access *)

  let test (a: sparse_array 'a) i
    requires { 0 <= i < length a }
    ensures { result=True <-> is_elt a i }
  = 0 <= a.index[i] < a.card && a.back[a.index[i]] = i

  let get (a: sparse_array 'a) i
    requires { 0 <= i < length a }
    ensures { result = value a i }
  = if test a i then
      a.values[i]
    else
      a.def

  (* assignment *)

  use map.MapInjection as MI

  lemma permutation :
    forall a: sparse_array 'a.
    (* sparse_array invariant *)
      (0 <= a.card <= A.length a.values <= maxlen /\
      A.length a.values = A.length a.index = A.length a.back /\
      forall i : int.
        0 <= i < a.card ->
        0 <= a.back[i] < A.length a.values /\ a.index[a.back[i]] = i) ->
    (* sparse_array invariant *)
    a.card = a.length ->
    forall i: int. 0 <= i < a.length -> is_elt a i

  let set (a: sparse_array 'a) i v
    requires { 0 <= i < length a }
    ensures { value a i = v /\
      forall j:int. j <> i -> value a j = value (old a) j }
  = a.values[i] <- v;
    if not (test a i) then begin
      assert { a.card < length a };
      a.index[i] <- a.card;
      a.back[a.card] <- i;
      a.card <- a.card + 1
    end

end

module Harness

  use import SparseArray

  type elt
  constant default : elt

  constant c1 : elt
  constant c2 : elt

  let harness () =
    let a = create 10 default in
    let b = create 20 default in
    let get_a_5 = get a 5 in assert { get_a_5 = default };
    let get_b_7 = get b 7 in assert { get_b_7 = default };
    set a 5 c1;
    set b 7 c2;
    let get_a_5 = get a 5 in assert { get_a_5 = c1 };
    let get_b_7 = get b 7 in assert { get_b_7 = c2 };
    let get_a_7 = get a 7 in assert { get_a_7 = default };
    let get_b_5 = get b 5 in assert { get_b_5 = default };
    let get_a_0 = get a 0 in assert { get_a_0 = default };
    let get_b_0 = get b 0 in assert { get_b_0 = default };
    ()

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let a = create 10 default in
    let b = create 20 default in
    if get a 5 <> default then raise BenchFailure;
    if get b 7 <> default then raise BenchFailure;
    set a 5 c1;
    set b 7 c2;
    if get a 5 <> c1 then raise BenchFailure;
    if get b 7 <> c2 then raise BenchFailure;
    if get a 7 <> default then raise BenchFailure;
    if get b 5 <> default then raise BenchFailure;
    if get a 0 <> default then raise BenchFailure;
    if get b 0 <> default then raise BenchFailure

end

download ZIP archive

Why3 Proof Results for Project "vacid_0_sparse_array"

Theory "vacid_0_sparse_array.SparseArray": fully verified in 2.86 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Coq (8.4pl6)Z3 (3.2)
VC for create0.02---------
VC for test0.18---------
VC for get0.07---------
permutation------1.40---
VC for set------------
split_goal_wp
  1. index in array bounds0.01---------
2. type invariant0.02---------
3. type invariant0.01---------
4. precondition0.03---------
5. assertion0.030.09---0.02
6. index in array bounds0.02---------
7. index in array bounds0.03---------
8. type invariant---0.05---0.02
9. type invariant0.04---------
10. type invariant0.04---------
11. postcondition------------
split_goal_wp
  1. VC for set0.10---------
2. VC for set1.120.52---0.02
12. postcondition0.17---------

Theory "vacid_0_sparse_array.Harness": fully verified in 0.45 s

ObligationsAlt-Ergo (0.99.1)
VC for harness0.39
VC for bench0.06