impset.mlw 668 Bytes
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3
(** {1 Imperative sets}

4
An imperative set is simply a reference containing a finite set.
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7

*)

8
module Impset
Jean-Christophe's avatar
Jean-Christophe committed
9 10

  use export set.Fset
11
  use export ref.Ref
Jean-Christophe's avatar
Jean-Christophe committed
12 13 14

  type t 'a = ref (set 'a)

15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
  let empty () ensures { is_empty !result } = ref (empty : set 'a)

  let create (s: set 'a) ensures { !result = s } = ref s

  let is_empty (b: t 'a) ensures { result = True <-> is_empty !b }
  = is_empty !b

  let push (x: 'a) (b: t 'a) ensures { !b = add x (old !b) }
  = b := add x !b

  let pop (b: t 'a)
    requires { not (is_empty !b) }
    ensures  { mem result (old !b) }
    ensures  { !b = remove result (old !b) }
  = let x = choose !b in
Jean-Christophe's avatar
Jean-Christophe committed
30 31 32 33
    b := remove x !b;
    x

end