Why3 Standard Library index



Imperative sets

An imperative set is simply a reference containing a finite set.

module Impset

  use export set.Fset
  use export ref.Ref

  type t 'a = ref (set 'a)

  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
    b := remove x !b;
    x

end

Generated by why3doc 0.87.3