/usr/share/why3/modules/hashtbl.mlw is in why3 0.88.3-1ubuntu4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 53 54 55 56 57 58 59 60 61 62 63 | (** {1 Hash tables}
This module provides Hash tables à la OCaml.
Each key is mapped to a {h <b>stack</b>} of values,
with [add h k v] pushing a new value [v] for key [k],
and [remove h k] popping a value for key [k].
*)
module Hashtbl
use import list.List
use import map.Map
type key
type t 'a model { mutable contents: map key (list 'a) }
function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
val create (n:int) : t 'a ensures { forall k: key. result[k] = Nil }
val clear (h: t 'a) : unit writes {h} ensures { forall k: key. h[k] = Nil }
val add (h: t 'a) (k: key) (v: 'a) : unit writes {h}
ensures { h[k] = Cons v (old h)[k] }
ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
val mem (h: t 'a) (k: key) : bool
ensures { result=True <-> h[k] <> Nil }
val find (h: t 'a) (k: key) : 'a
requires { h[k] <> Nil }
ensures { match h[k] with Nil -> false | Cons v _ -> result = v end }
val find_all (h: t 'a) (k: key) : list 'a
ensures { result = h[k] }
exception NotFound
val defensive_find (h: t 'a) (k: key) : 'a
ensures { match h[k] with Nil -> false | Cons v _ -> result = v end }
raises { NotFound -> h[k] = Nil }
val copy (h: t 'a) : t 'a
ensures { forall k: key. result[k] = h[k] }
val remove (h: t 'a) (k: key) : unit writes {h}
ensures { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end }
ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
val replace (h: t 'a) (k: key) (v: 'a) : unit writes {h}
ensures {
h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end) }
ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
(*** TODO
- val length: t 'a -> int (the number of distinct key)
- val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
- val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
*)
end
|