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 val +-----+-+---+-+----+-+----+ | |y| |x| |z| | +-----+-+---+-+----+-+----+ idx +-----+-+---+-+----+-+----+ | |1| |0| |2| | +-----+-+---+-+----+-+----+ 0 1 2 n=3 back +-+-+-+-------------------+ |a|b|c| | +-+-+-+-------------------+ *) use import int.Int use import module array.Array as A type sparse_array 'a = {| val : array 'a; idx : array int; back : array int; mutable card : int; default : 'a; |} logic is_elt (a: sparse_array 'a) (i: int) = 0 <= a.idx[i] < a.card and a.back[a.idx[i]] = i logic value (a: sparse_array 'a) (i: int) : 'a = if is_elt a i then a.val[i] else a.default (* invariant *) logic maxlen : int = 1000 logic length (a: sparse_array 'a) : int = A.length a.val logic sa_inv (a: sparse_array 'a) = 0 <= a.card <= length a <= maxlen and A.length a.val = A.length a.idx = A.length a.back and forall i : int. 0 <= i < a.card -> 0 <= a.back[i] < length a and a.idx[a.back[i]] = i (* creation *) parameter malloc : n:int -> {} array 'a { A.length result = n } let create (sz: int) (d: 'a) = { 0 <= sz <= maxlen } {| val = malloc sz; idx = malloc sz; back = malloc sz; card = 0; default = d |} { sa_inv result and result.card = 0 and result.default = d and length result = sz } (* access *) let test (a: sparse_array 'a) i = { 0 <= i < length a and sa_inv a } 0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i { result=True <-> is_elt a i } let get (a: sparse_array 'a) i = { 0 <= i < length a and sa_inv a } if test a i then a.val[i] else a.default { result = value a i } (* assignment *) lemma permutation : forall a: sparse_array 'a. sa_inv a -> a.card = a.length -> forall i: int. 0 <= i < a.length -> is_elt a i let set (a: sparse_array 'a) i v = { 0 <= i < length a and sa_inv a } a.val[i] <- v; if not (test a i) then begin assert { a.card < length a }; a.idx[i] <- a.card; a.back[a.card] <- i; a.card <- a.card + 1 end { sa_inv a and value a i = v and forall j:int. j <> i -> value a j = value (old a) j } end module Harness use import module SparseArray type elt logic default : elt logic c1 : elt logic 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 }; () end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_sparse_array.gui" End: *)