examples/vacid_0_sparse_array.mlw

   1 module SparseArray
   2
   3 (*
   4       If the sparse array contains three elements x y z, at index
   5       a b c respectively, then the three arrays look like this:
   6
   7               b     a      c
   8 values +-----+-+---+-+----+-+----+
   9        |     |y|   |x|    |z|    |
  10        +-----+-+---+-+----+-+----+
  11
  12 index  +-----+-+---+-+----+-+----+
  13        |     |1|   |0|    |2|    |
  14        +-----+-+---+-+----+-+----+
  15
  16         0 1 2  n=3
  17 back   +-+-+-+-------------------+
  18        |a|b|c|                   |
  19        +-+-+-+-------------------+
  20
  21 *)
  22
  23   use int.Int
  24   use array.Array
  25
  26   constant maxlen : int = 1000
  27
  28   type sparse_array 'a = { values : array 'a;
  29                            index  : array int;
  30                            back   : array int;
  31                    mutable card   : int;
  32                            def    : 'a; }
  33   invariant {
  34     0 <= card <= length values <= maxlen /\
  35     length values = length index = length back /\
  36     forall i : int.
  37       0 <= i < card ->
  38       0 <= back[i] < length values /\ index[back[i]] = i
  39   } by {
  40     values = make 0 (any 'a);
  41     index  = make 0 0;
  42     back   = make 0 0;
  43     card   = 0;
  44     def    = any 'a
  45   }
  46
  47   predicate is_elt (a: sparse_array 'a) (i: int) =
  48     0 <= a.index[i] < a.card /\ a.back[a.index[i]] = i
  49
  50   function value (a: sparse_array 'a) (i: int) : 'a =
  51     if is_elt a i then
  52       a.values[i]
  53     else
  54       a.def
  55
  56   function length (a: sparse_array 'a) : int = Array.length a.values
  57
  58   (* creation *)
  59
  60   val malloc (n:int) : array 'a ensures { Array.length result = n }
  61
  62   let create (sz: int) (d: 'a)
  63     requires { 0 <= sz <= maxlen }
  64     ensures { result.card = 0 /\ result.def = d /\ length result = sz }
  65   = { values = malloc sz;
  66       index  = malloc sz;
  67       back   = malloc sz;
  68       card   = 0;
  69       def    = d }
  70
  71   (* access *)
  72
  73   let test (a: sparse_array 'a) i
  74     requires { 0 <= i < length a }
  75     ensures { result=True <-> is_elt a i }
  76   = 0 <= a.index[i] < a.card && a.back[a.index[i]] = i
  77
  78   let get (a: sparse_array 'a) i
  79     requires { 0 <= i < length a }
  80     ensures { result = value a i }
  81   = if test a i then
  82       a.values[i]
  83     else
  84       a.def
  85
  86   (* assignment *)
  87
  88   use map.MapInjection as MI
  89
  90   lemma permutation :
  91     forall a: sparse_array 'a.
  92     (* sparse_array invariant *)
  93       Array.(0 <= a.card <= Array.length a.values <= maxlen /\
  94       length a.values = length a.index = length a.back /\
  95       forall i : int.
  96         0 <= i < a.card ->
  97         0 <= a.back[i] < length a.values /\ a.index[a.back[i]] = i) ->
  98     (* sparse_array invariant *)
  99     a.card = a.length ->
 100     forall i: int. 0 <= i < a.length -> is_elt a i
 101       by MI.surjective a.back.elts a.card
 102       so exists j. 0 <= j < a.card /\ a.back[j] = i
 103
 104
 105   let set (a: sparse_array 'a) i v
 106     requires { 0 <= i < length a }
 107     ensures { value a i = v /\
 108       forall j:int. j <> i -> value a j = value (old a) j }
 109   = a.values[i] <- v;
 110     if not (test a i) then begin
 111       assert { a.card < length a };
 112       a.index[i] <- a.card;
 113       a.back[a.card] <- i;
 114       a.card <- a.card + 1
 115     end
 116
 117 end
 118
 119 module Harness
 120
 121   use SparseArray
 122
 123   type elt
 124   val constant default : elt
 125
 126   val constant c1 : elt
 127   val constant c2 : elt
 128
 129   let harness () =
 130     let a = create 10 default in
 131     let b = create 20 default in
 132     let get_a_5 = get a 5 in assert { get_a_5 = default };
 133     let get_b_7 = get b 7 in assert { get_b_7 = default };
 134     set a 5 c1;
 135     set b 7 c2;
 136     let get_a_5 = get a 5 in assert { get_a_5 = c1 };
 137     let get_b_7 = get b 7 in assert { get_b_7 = c2 };
 138     let get_a_7 = get a 7 in assert { get_a_7 = default };
 139     let get_b_5 = get b 5 in assert { get_b_5 = default };
 140     let get_a_0 = get a 0 in assert { get_a_0 = default };
 141     let get_b_0 = get b 0 in assert { get_b_0 = default };
 142     ()
 143
 144   val predicate (!=) (x y : elt)
 145     ensures { result <-> x <> y }
 146
 147   exception BenchFailure
 148
 149   let bench () raises { BenchFailure -> true } =
 150     let a = create 10 default in
 151     let b = create 20 default in
 152     if get a 5 != default then raise BenchFailure;
 153     if get b 7 != default then raise BenchFailure;
 154     set a 5 c1;
 155     set b 7 c2;
 156     if get a 5 != c1 then raise BenchFailure;
 157     if get b 7 != c2 then raise BenchFailure;
 158     if get a 7 != default then raise BenchFailure;
 159     if get b 5 != default then raise BenchFailure;
 160     if get a 0 != default then raise BenchFailure;
 161     if get b 0 != default then raise BenchFailure
 162
 163 end