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

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

4
module Impset
MARCHE Claude's avatar
MARCHE Claude committed
5

6
  use set.Fset
MARCHE Claude's avatar
MARCHE Claude committed
7

8 9 10
  type elt

  type t = abstract { mutable contents: set elt }
Jean-Christophe's avatar
Jean-Christophe committed
11

12
  val empty (): t
13
    ensures { is_empty result.contents }
Jean-Christophe's avatar
Jean-Christophe committed
14

15 16 17 18 19
  val clear (s: t): unit
    writes  { s }
    ensures { is_empty s.contents }

  val predicate is_empty (s: t)
20
    ensures { result <-> is_empty s.contents }
Jean-Christophe's avatar
Jean-Christophe committed
21

22
  val predicate mem (x: elt) (s: t)
23
    ensures { result <-> mem x s.contents }
24

25
  val add (x: elt) (s: t): unit
26 27
    writes  { s }
    ensures { s.contents = add x (old s.contents) }
28

29 30 31
  val choose (s: t): elt
    requires { not (is_empty s) }
    ensures  { mem result s }
32

33
  val remove (x: elt) (s: t): unit
34 35
    writes   { s }
    ensures  { s.contents = remove x (old s.contents) }
36

37 38 39 40
  val choose_and_remove (s: t): elt
    writes   { s }
    requires { not (is_empty s) }
    ensures  { mem result (old s) }
41
    ensures  { s.contents = remove result (old s.contents) }
42 43 44

  val function cardinal (s: t): int
    ensures { result = cardinal s.contents }
Jean-Christophe's avatar
Jean-Christophe committed
45 46

end