Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Sparse Arrays in Capucine

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


Authors: Claude Marché / Romain Bardou

Topics: Array Data Structure / Permutation / Separation challenges

Tools: Capucine / Coq

References: The VACID-0 Benchmarks / The VerifyThis Benchmarks

See also: Sparse Arrays in Why3

index


The following code is the Sparse Arrays Verification Challenge from the VACID0 benchmark [4].

A first challenge is to handle enough separation information so that the test Harness involving two disjoint sparse arrasy can be proved. A second challenge is the assertion in the code of add() to show that the array is not accessed outside its bound: the proof requires to reason about permutation, more precisely we used a mathematical lemma proved in Coq that an injection over a finite set is also a surjection.

See Romain Bardou’s PhD [1] for more details.

References

[1]
Romain Bardou. Verification of Pointer Programs Using Regions and Permissions. Thèse de doctorat, Université Paris-Sud, 2011. http://romain.bardou.fr/thesis/bardou11phd.pdf.
[2]
Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Research Report 7412, INRIA, 2010. http://hal.inria.fr/inria-00525384/en/.
[3]
Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA.
[4]
K. Rustan M. Leino and Michał Moskal. VACID-0: Verification of ample correctness of invariants of data-structures, edition 0. In Proceedings of Tools and Experiments Workshop at VSTTE, 2010.

(* Logic (Infinite) Arrays *)
logic type array (alpha)
logic function store (array (alpha), int, alpha): array (alpha)
logic function select (array (alpha), int): alpha

axiom select_eq:
  forall a: array (alpha).
  forall i: int.
  forall v: alpha.
  [select(store(a, i, v), i)] = [v]

axiom select_neq:
  forall a: array (alpha).
  forall i: int.
  forall j: int.
  forall v: alpha.
  [i] <> [j] ==>
  [select(store(a, i, v), j)] = [select(a, j)]



(* Array Reference *)
selector (length, cell)
class Array (alpha) =
  (int * array (alpha))
  invariant(a) = [0] <= [a.length]
end



val array_get(a: Array (alpha) [R], i:int) : alpha
  requires [0] <= [i] and [i] < [!a.length]
  ensures [result] = [select(!a.cell,i)] =
      select(!a.cell,i)



val array_set(a: Array (alpha) [R], i:int, v:alpha) : unit
  consumes R^c
  produces R^c
  requires [0] <= [i] and [i] < [!a.length]
  ensures [!a.length] = [old(!a.length)] and
          [!a.cell] = [store(old(!a.cell),i,v)]
  =
      (a := (!a.length, store(!a.cell,i,v)))



val array_create(size:int): Array (alpha) [R]
  consumes R^e
  produces R^c
  requires [0] <= [size]
  ensures [!result.length] = [size] =
    let tmp = new Array (alpha) in
    tmp := (size, !tmp.cell);
    tmp






(* Sparse Arrays *)



predicate interval(a:int, x:int, b:int) = [a] <= [x] and [x] < [b]


selector (value, idx, back, n, default, size)
(* value: actual values at their actual indexes
   idx: corresponding indexes in back
   back: corresponding indexes in idx, makes sense between 0 and n-1
   n: see back
   size: allocated size
*)

class Sparse (alpha) =
  own Rval, Ridx, Rback;

  (Array (alpha) [Rval] * Array (int) [Ridx] * Array (int) [Rback] *
   int * alpha * int)

  invariant (x) =
    [0] <= [x.n] and [x.n] <= [x.size] and
    [!(x.value).length] = [x.size] and
    [!(x.idx).length] = [x.size] and
    [!(x.back).length] = [x.size] and
    forall i: int. interval([0],[i],[x.n]) ==>
      interval([0],[select (!(x.back).cell, i)],[x.size]) and
      [select (!(x.idx).cell, select (!(x.back).cell, i))] = [i]
end




(* is_elt(a,i) tells whether index i points to a existing element. It
  can be checked as follows:

  (1) check that array idx maps i to a index j between 0 and n (excluded)
  (2) check that back(j) is i
*)

predicate is_elt(a: Sparse (alpha) [R], i: int) =
  [0] <= [select (!(!a.idx).cell, i)]
  and [select (!(!a.idx).cell, i)] < [!a.n]
  and [select (!(!a.back).cell, select (!(!a.idx).cell, i))] = [i]






logic function model (Sparse (alpha) [R], int): alpha

axiom model_in:
  forall a: Sparse (alpha) [R].
  forall i: int.
  is_elt([a], [i]) ==> [model(a, i)] = [select(!(!a.value).cell, i)]

axiom model_out:
  forall a: Sparse (alpha) [R].
  forall i: int.
  not is_elt([a], [i]) ==> [model(a, i)] = [!a.default]






val create(sz:int, def: alpha): Sparse (alpha) [R]
  consumes R^e
  produces R^c
  requires
    [0] <= [sz]
  ensures
    [!result.size] = [sz] and
    forall i: int. [model (result, i)] = [def]
  =
    let arr = new Sparse (alpha) in
    arr := (array_create (sz), array_create (sz),
            array_create (sz), 0, def, sz);
    arr




val get(a: Sparse (alpha) [R], i: int): alpha
  consumes R^c
  produces R^c
  requires [0] <= [i] and [i] < [!a.size]
  ensures [result] = [model(a, i)] =
    let index = array_get(!a.idx, i) in
    if 0 <= index and index < !a.n and array_get(!a.back, index) = i
    then
      array_get(!a.value, i)
    else
      !a.default





val set(a: Sparse (alpha) [R], i: int, v: alpha): unit
  consumes R^c
  produces R^c
  requires [0] <= [i] and [i] < [!a.size]
  ensures
    [!a.size] = [old(!a.size)] and
    (forall j: int. [j] <> [i] ==> [model(a, j)] = [old(model(a, j))])
    and ([model(a, i)] = [v])
  =
    array_set((focus !a.value), i, v);
    let index = array_get(!a.idx, i) in
    if not (0 <= index and index < !a.n and array_get(!a.back, index) = i)
    then (
        (* the hard assertion! *)
        assert [!a.n] < [!a.size];
        array_set((focus !a.idx), i, !a.n);
        array_set((focus !a.back), !a.n, i);
        a := (!a.value, !a.idx, !a.back, !a.n + 1, !a.default, !a.size)
    )


val main(): unit =
  region Ra: Sparse (int) in
  region Rb: Sparse (int) in
  let default = 0 in
  let a = (create(10,default): Sparse (int) [Ra]) in
  let b = (create(20,default): Sparse (int) [Rb]) in
  let x = get(a, 5) in
  let y = get(b, 7) in
  assert ([x] = [default] and [y] = [default]);
  set(a, 5, 1);
  set(b, 7, 2);
  let x = get(a, 5) in
  let y = get(b, 7) in
  assert ([x] = [1] and [y] = [2]);
  let x = get(a, 7) in
  let y = get(b, 5) in
  assert ([x] = [default] and [y] = [default]);
  let x = get(a, 0) in
  let y = get(b, 0) in
  assert ([x] = [default] and [y] = [default]);
  let x = get(a, 9) in
  let y = get(b, 9) in
  assert ([x] = [default] and [y] = [default]);
  assert false (* poorman's check for inconsistency *)