library: applicative/mutable maps and sets

parent 7bff4e2b
(** {2 Applicative sets} *)
module Appset
use import set.Fset
type elt
type t = abstract { contents: set elt }
val constant empty: t
ensures { is_empty result.contents }
val predicate is_empty (s: t) : bool
ensures { result <-> is_empty s.contents }
val function add (x: elt) (s: t) : t
ensures { result.contents = add x s.contents }
val function remove (x: elt) (s: t) : t
ensures { result.contents = remove x s.contents }
val predicate mem (x: elt) (s: t) : bool
ensures { result <-> mem x s.contents }
val predicate (==) (s1 s2: t) : bool
ensures { result <-> s1.contents == s2.contents }
val predicate subset (s1 s2: t) : bool
ensures { result <-> subset s1.contents s2.contents }
val function union (s1 s2: t) : t
ensures { result.contents = union s1.contents s2.contents }
val function inter (s1 s2: t) : t
ensures { result.contents = inter s1.contents s2.contents }
val function diff (s1 s2: t) : t
ensures { result.contents = diff s1.contents s2.contents }
val function choose (s: t) : elt
requires { not (Fset.is_empty s.contents) }
ensures { Fset.mem result s.contents }
val function cardinal (s: t) : int
ensures { result = cardinal s.contents }
end
(** {2 General-purpose exceptions} *)
module Exn
exception Not_found
exception Exit
end
(** {1 Imperative maps with finite domain} *)
module Impmap
use import option.Option
use import map.Map
use import map.MapExt
use export exn.Exn
type key
type t 'a = abstract {
mutable contents: map key (option 'a)
}
val empty () : t 'a
ensures { result.contents = const None }
val is_empty (m: t 'a) : bool
ensures { result <-> m.contents == const None }
val mem (k: key) (m: t 'a) : bool
ensures { result <-> m.contents[k] <> None }
val get (k: key) (m: t 'a) : 'a
requires { m.contents[k] <> None }
ensures { m.contents[k] = Some result }
val get_opt (k: key) (m: t 'a) : option 'a
ensures { result = m.contents[k] }
val get_def (k: key) (d: 'a) (m: t 'a) : 'a
ensures { result = match m.contents[k] with None -> d | Some v -> v end }
val find (k: key) (m: t 'a) : 'a
ensures { m.contents[k] = Some result }
raises { Not_found -> m.contents[k] = None }
val add (k: key) (v: 'a) (m: t 'a) : unit
writes { m }
ensures { m.contents = old m.contents[k <- Some v] }
val remove (k: key) (m: t 'a) : unit
writes { m }
ensures { m.contents = old m.contents[k <- None] }
end
(** {1 Imperative sets}
(** {1 Imperative sets} *)
An imperative set is simply a reference containing a finite set.
module Impset
*)
use import set.Fset
module Impset
type elt
type t = abstract { mutable contents: set elt }
use export set.Fset
use export ref.Ref
val empty () : t
ensures { is_empty result.contents }
type t 'a = ref (set 'a)
val is_empty (s: t) : bool
ensures { result <-> is_empty s.contents }
let empty () ensures { is_empty !result } = ref (empty : set 'a)
val mem (x: elt) (s: t) : bool
ensures { result <-> mem x s.contents }
let create (s: set 'a) ensures { !result = s } = ref s
val add (x: elt) (s: t) : unit
writes { s }
ensures { s.contents = add x (old s.contents) }
let is_empty (b: t 'a) ensures { result = True <-> is_empty !b }
= is_empty !b
val choose (s: t) : elt
requires { not (is_empty s.contents) }
ensures { mem result s.contents }
let push (x: 'a) (b: t 'a) ensures { !b = add x (old !b) }
= b := add x !b
val remove (x: elt) (s: t) : unit
writes { s }
ensures { s.contents = remove x (old s.contents) }
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;
let choose_and_remove (s: t) : elt
requires { not (is_empty s.contents) }
ensures { mem result (old s.contents) }
ensures { s.contents = remove result (old s.contents) }
= let x = choose s in
remove x s;
x
end
......@@ -42,6 +42,15 @@ theory Map
end
theory MapExt
predicate (==) (m1 m2: 'a -> 'b) = forall x: 'a. m1 x = m2 x
axiom extensionality:
forall m1 m2: 'a -> 'b. m1 == m2 -> m1 = m2
end
(** {2 Sorted Maps (indexed by integers)} *)
theory MapSorted
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment