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 / Data Structures
References: The VACID-0 Benchmarks / The VerifyThis Benchmarks
See also: Sparse Arrays in Why3
see also the index (by topic, by tool, by reference, by year)
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 *)