vacid_0_sparse_array.mlw 3.33 KB
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1
module SparseArray
2

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

MARCHE Claude's avatar
MARCHE Claude committed
7
             b     a      c
8 9 10 11 12
val   +-----+-+---+-+----+-+----+
      |     |y|   |x|    |z|    |
      +-----+-+---+-+----+-+----+

idx   +-----+-+---+-+----+-+----+
MARCHE Claude's avatar
MARCHE Claude committed
13
      |     |1|   |0|    |2|    |
14 15 16 17 18 19 20 21 22
      +-----+-+---+-+----+-+----+

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

*)

23
  use import int.Int
24
  use import module array.Array as A
25

Jean-Christophe's avatar
Jean-Christophe committed
26 27 28 29 30
  type sparse_array 'a = {| val  : array 'a;
                            idx  : array int;
                            back : array int;
                    mutable card : int;
                         default : 'a; |}
31

Jean-Christophe's avatar
Jean-Christophe committed
32
  logic is_elt (a: sparse_array 'a) (i: int) =
33
    0 <= a.idx[i] < a.card and a.back[a.idx[i]] = i
34

35
  logic value (a: sparse_array 'a) (i: int) : 'a =
36
    if is_elt a i then
37
      a.val[i]
38
    else
Jean-Christophe's avatar
Jean-Christophe committed
39
      a.default
40

Jean-Christophe's avatar
Jean-Christophe committed
41 42 43 44 45 46 47
  (* invariant *)

  logic maxlen : int = 1000

  logic length (a: sparse_array 'a) : int = A.length a.val

  logic sa_inv (a: sparse_array 'a) =
48 49 50 51 52
    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
53

Jean-Christophe's avatar
Jean-Christophe committed
54
  (* creation *)
55

56
  parameter malloc : n:int -> {} array 'a { A.length result = n }
57

Jean-Christophe's avatar
Jean-Christophe committed
58
  let create (sz: int) (d: 'a) =
59
    { 0 <= sz <= maxlen }
Jean-Christophe's avatar
Jean-Christophe committed
60 61 62 63 64
    {| val = malloc sz; 
       idx = malloc sz; 
       back = malloc sz; 
       card = 0; 
       default = d |}
Jean-Christophe's avatar
Jean-Christophe committed
65
    { sa_inv result and result.card = 0 and 
66
      result.default = d and length result = sz }
67

Jean-Christophe's avatar
Jean-Christophe committed
68 69
  (* access *)

Jean-Christophe's avatar
Jean-Christophe committed
70
  let test (a: sparse_array 'a) i =
Jean-Christophe's avatar
Jean-Christophe committed
71
    { 0 <= i < length a and sa_inv a }
72
    0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i
73 74
    { result=True <-> is_elt a i }

Jean-Christophe's avatar
Jean-Christophe committed
75
  let get (a: sparse_array 'a) i =
Jean-Christophe's avatar
Jean-Christophe committed
76
    { 0 <= i < length a and sa_inv a }
77
    if test a i then
Jean-Christophe's avatar
Jean-Christophe committed
78
      a.val[i]
79
    else
Jean-Christophe's avatar
Jean-Christophe committed
80
      a.default
81
    { result = value a i }
82

Jean-Christophe's avatar
Jean-Christophe committed
83 84 85 86 87 88 89
  (* 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

Jean-Christophe's avatar
Jean-Christophe committed
90
  let set (a: sparse_array 'a) i v =
Jean-Christophe's avatar
Jean-Christophe committed
91
    { 0 <= i < length a and sa_inv a }
92
    a.val[i] <- v;
93
    if not (test a i) then begin
94 95 96 97
      assert { a.card < length a };
      a.idx[i] <- a.card;
      a.back[a.card] <- i;
      a.card <- a.card + 1
98
    end
Jean-Christophe's avatar
Jean-Christophe committed
99
    { sa_inv a and
100 101
      value a i = v and
      forall j:int. j <> i -> value a j = value (old a) j }
102

Jean-Christophe's avatar
Jean-Christophe committed
103 104 105 106 107 108 109 110 111 112 113 114
end

module Harness

  use import module SparseArray

  type elt
  logic default : elt

  logic c1 : elt
  logic c2 : elt

115
  let harness () =
Jean-Christophe's avatar
Jean-Christophe committed
116 117
    let a = create 10 default in
    let b = create 20 default in
118 119 120 121 122 123 124 125 126 127 128
    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 };
    ()
129

130 131
end

132
(*
MARCHE Claude's avatar
MARCHE Claude committed
133
Local Variables:
134
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_sparse_array.gui"
MARCHE Claude's avatar
MARCHE Claude committed
135
End:
136
*)