bag.mlw 4.32 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52

module Bag

  use import HighOrd
  use import int.Int

  type bag 'a = 'a -> int

  predicate (==) (b1 b2: bag 'a) =
    forall x: 'a. b1 x = b2 x

  constant empty : bag 'a =
    \ _. 0

  function add (e: 'a) (b: bag 'a) : bag 'a =
    \ x. if x = e then b x + 1 else b x

  function remove (e: 'a) (b: bag 'a) : bag 'a =
    \ x. if x = e then b x - 1 else b x

end

module BagSpec

  use import int.Int
  use import Bag

  type t 'a model {
    mutable size: int;
    mutable contents: bag 'a;
  }

  val create () : t 'a
    ensures { result.size = 0 }
    ensures { result.contents == Bag.empty }

  val clear (t: t 'a) : unit
    writes  { t.size, t.contents }
    ensures { t.size = 0 }
    ensures { t.contents == Bag.empty }

  val add (t: t 'a) (x: 'a) : unit
    writes  { t.size, t.contents }
    ensures { t.size = old t.size + 1 }
    ensures { t.contents == Bag.add x (old t.contents) }

end

module ResizableArraySpec

  use import int.Int
  use import map.Map
53
  use map.Const
54 55 56 57 58 59 60 61 62 63 64 65 66

  type rarray 'a model { mutable length: int; mutable data: map int 'a }

  function ([]) (r: rarray 'a) (i: int) : 'a = Map.get r.data i
  function ([<-]) (r: rarray ~'a) (i: int) (v: 'a) : rarray 'a =
    { r with data = Map.set r.data i v }

  val length (r: rarray ~'a) : int
    ensures { result = r.length }

  val make (len: int) (dummy: ~'a) : rarray 'a
    requires { 0 <= len }
    ensures  { result.length = len }
67
    ensures  { result.data = Const.const dummy }
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153

  val ([]) (r: rarray ~'a) (i: int) : 'a
    requires { 0 <= i < r.length }
    ensures  { result = r[i] }

  val ([]<-) (r: rarray ~'a) (i: int) (v: 'a) : unit
    requires { 0 <= i < r.length }
    writes   { r.data }
    ensures  { r = (old r)[i <- v] }

  val resize (r: rarray ~'a) (len: int) : unit
    requires { 0 <= len }
    writes   { r.length, r.data }
    ensures  { r.length = len }
    ensures  { forall i: int.
               0 <= i < old r.length -> i < len -> r[i] = (old r)[i] }

end

module BagImpl

  use import int.Int
  use import Bag
  use import ResizableArraySpec as R
  use map.Map
  use int.NumOf
  use null.Null

  function numof (r: rarray (Null.t 'a)) (x: 'a) (l u: int) : int =
    NumOf.numof (\i. (Map.get r.R.data i).Null.v = Null.Value x) l u

  type t 'a = {
    mutable       size:     int;
                  data:     rarray (Null.t 'a);
    mutable ghost contents: bag 'a;
  }
  invariant { 0 <= self.size = self.data.length }
  invariant { forall i: int. 0 <= i < self.size ->
                not (Null.is_null self.data[i]) }
  invariant { forall x: 'a. self.contents x = numof self.data x 0 self.size }

  let create () : t 'a
    ensures { result.size = 0 }
    ensures { result.contents == Bag.empty }
  =
    let null = Null.create_null () : Null.t 'a in
    { size = 0; data = make 0 null; contents = Bag.empty }

  let clear (t: t 'a) : unit
    ensures { t.size = 0 }
    ensures { t.contents == Bag.empty }
  =
    resize t.data 0;
    t.size <- 0;
    t.contents <- Bag.empty

  let add (t: t 'a) (x: 'a) : unit
    ensures { t.size = old t.size + 1 }
    ensures { t.contents == Bag.add x (old t.contents) }
  =
    let n = t.size in
    resize t.data (n + 1);
    t.data[n] <- (Null.create x);
    t.size <- n + 1;
    t.contents <- Bag.add x t.contents

  let get (t: t 'a) (i: int) : 'a
    requires { 0 <= i < t.size }
    ensures  { Null.Value result = t.data[i].Null.v }
  =
    Null.get t.data[i]

  let remove (t: t 'a) (i: int) : unit
    requires { 0 <= i < t.size }
    ensures  { t.size = old t.size - 1 }
    ensures  { forall x: 'a. Null.Value x = old t.data[i].Null.v ->
               t.contents == Bag.remove x (old t.contents) }
  =
    'L:
    let n = t.size - 1 in
    let ghost x = Null.get t.data[i] in
    if i < n then t.data[i] <- t.data[n];
    resize t.data n;
    t.size <- n;
    t.contents <- Bag.remove x t.contents;
    assert { forall v: 'a. numof t.data v 0 i = numof (at t.data 'L) v 0 i };
154
    assert { forall v: 'a.
155 156 157
             numof t.data v i n = numof (at t.data 'L) v (i+1) (n+1) };
    assert { forall v: 'a.
             numof t.data v 0 n = numof t.data v 0 i + numof t.data v i n }
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178

end

module Harness

  use import int.Int
  use import Bag
  use import BagImpl

  let test1 () =
    let b = create () in
    add b 17;
    add b 42;
    assert { b.contents 42 = 1 };
    add b 55;
    add b 89;
    add b 42;
    assert { b.contents 42 = 2 };
    ()

end