spec/containers/hash_table.bend source
spec/containers/hash_table.bend on the hub · documented module
import Baseimport ../lib/common.bend as SCimport ../../src/containers/hash_table.bend as H# Independent model: a map from String keys to values is an association# list with at most one entry per key. Nothing here refers to buckets,# hashing, probing or slots.type Entry<-V: Data> is Data: E{key: String, val: V}def chr_eq(a: Char, b: Char) -> Bool: match a b: case Chr{x} Chr{y}: U32.is_eq(x, y)def str_eq(a: String, b: String) -> Bool: match a b: case SNil{} SNil{}: True{} case SNil{} SCon{h, t}: False{} case SCon{h, t} SNil{}: False{} case SCon{x, s} SCon{y, t}: Bool.and(chr_eq(x, y), str_eq(s, t))def lookup(~V: Data, m: List<&2, Entry<V>>, +k: String) -> Maybe<&2, V>: match m: case Nil{}: None{} case Con{E{+j, +v}, t}: Bool.pick(Maybe<&2, V>, str_eq(j, k), Some{v}, lookup(~V, t, k))def is_some(~V: Data, m: Maybe<&2, V>) -> Bool: match m: case None{}: False{} case Some{v}: True{}def has(~V: Data, m: List<&2, Entry<V>>, +k: String) -> Bool: is_some(~V, lookup(~V, m, k))# Replace the entry of k in place, or add it at the end.def set(~V: Data, m: List<&2, Entry<V>>, +k: String, +x: V) -> List<&2, Entry<V>>: match m: case Nil{}: Con{E{k, x}, Nil{}} case Con{E{+j, +v}, +t}: Bool.pick(List<&2, Entry<V>>, str_eq(j, k), Con{E{k, x}, t}, Con{E{j, v}, set(~V, t, k, x)})def remove(~V: Data, m: List<&2, Entry<V>>, +k: String) -> List<&2, Entry<V>>: match m: case Nil{}: Nil{} case Con{E{+j, +v}, +t}: Bool.pick(List<&2, Entry<V>>, str_eq(j, k), t, Con{E{j, v}, remove(~V, t, k)})def keys(~V: Data, m: List<&2, Entry<V>>) -> List<&2, String>: match m: case Nil{}: Nil{} case Con{E{j, v}, t}: Con{j, keys(~V, t)}def size(~V: Data, m: List<&2, Entry<V>>) -> Nat: match m: case Nil{}: 0n case Con{e, t}: 1n+size(~V, t)def mem(+k: String, ks: List<&2, String>) -> Bool: match ks: case Nil{}: False{} case Con{j, t}: Bool.or(str_eq(j, k), mem(k, t))def nodup(ks: List<&2, String>) -> Bool: match ks: case Nil{}: True{} case Con{+j, +t}: Bool.and(Bool.not(mem(j, t)), nodup(t))def get_m(~V: Data, dflt: V, m: Maybe<&2, V>) -> V: match m: case None{}: dflt case Some{v}: v# the value of key, or dfltdef get(~V: Data, dflt: V, m: List<&2, Entry<V>>, +key: String) -> V: get_m(~V, dflt, lookup(~V, m, key))# ---- contract (SPARK formal containers) ----# Each `<Subprogram>.<clause>` definition below states one Post clause of# that SPARK subprogram, as a proposition on this model; the table names the# clauses. proofs/containers/hash_table/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the hash map in the style of SPARK's formal hashed maps# (SPARKlib spark-containers-formal-hashed_maps.ads). The proofs in# set/pop/keysw.bend relate every operation to the specification's# association list; this module states, per operation, what changes and# what is preserved, over three views of a map sh:# Model S.lookup(ST.model(sh), q) the value of every key q# Length S.size(ST.model(sh))# Keys S.keys(ST.model(sh)) the keys, in iteration order# Keys are compared by S.str_eq, which is an equivalence under which equal# keys are identical strings (so, like SPARK's Equivalent_Keys, every# function of a key, the hash included, agrees on equivalent keys).# SPARK's cursor model (Positions) has no counterpart: the map has no# cursors.## SPARK subprogram (hashed_maps.ads line, AdaCore/SPARKlib master) ours lemmas# Empty_Map (103) new new_model, new_length, new_absent# Length (117) size length_value, length_frame (P.size_ok)# Element (Key) (1039) get element_value, element_default (P.get_ok)# Contains (1032) has contains_value (P.has_ok)# Include (729) set SetContract / SetPost (set_post)# Delete (Key) (891), Exclude (851) pop, del PopContract, DelContract / DelPost# Iter_Model / Keys (1078) keys KeysContract / KeysPost# Equivalent_Keys str_eq key_refl, key_sym, key_trans, key_same, key_respect# Not in this API: "=", Capacity, Reserve_Capacity, Is_Empty, Clear,# Assign/Copy/Move, Replace_Element/Reference (by cursor), Insert (fails# if present) and Replace (fails if absent), which Include subsumes,# First/Next/Has_Element/Key (cursors), Find, Default_Modulus.# ---- keys ----# The key sequence (SPARK's Keys): no key twice, as long as the map, and# holding exactly the keys the model has.def KeysPost(~V: Data, m: List<&2, Entry<V>>) -> Type: {nodup(keys(~V, m)) == True{} : Bool} & ({SC.length(String, keys(~V, m)) == size(~V, m) : Nat} & (@+q: String -> {mem(q, keys(~V, m)) == has(~V, m, q) : Bool}))# ---- set (SPARK's Include: insert, or replace the value) ----def SetPost(~V: Data, m: List<&2, Entry<V>>, m2: List<&2, Entry<V>>, key: String, x: V) -> Type: {has(~V, m2, key) == True{} : Bool} & ((@+q: String -> @+hq: {str_eq(key, q) == True{} : Bool} -> {lookup(~V, m2, q) == Some{x} : Maybe<&2, V>}) & ((@+q: String -> @+hq: {str_eq(key, q) == False{} : Bool} -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ({size(~V, m2) == Bool.pick(Nat, has(~V, m, key), size(~V, m), 1n+size(~V, m)) : Nat} & ((@+q: String -> {mem(q, keys(~V, m2)) == Bool.or(str_eq(key, q), mem(q, keys(~V, m))) : Bool}) & ({nodup(keys(~V, m2)) == True{} : Bool} & (@+hp: {has(~V, m, key) == True{} : Bool} -> {keys(~V, m2) == keys(~V, m) : List<&2, String>}))))))# ---- pop and del (SPARK's Delete/Exclude) ----def DelPost(~V: Data, m: List<&2, Entry<V>>, m2: List<&2, Entry<V>>, key: String) -> Type: {has(~V, m2, key) == False{} : Bool} & ((@+q: String -> @+hq: {str_eq(key, q) == False{} : Bool} -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ((@+hn: {has(~V, m, key) == False{} : Bool} -> @+q: String -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ({Bool.pick(Nat, has(~V, m, key), 1n+size(~V, m2), size(~V, m2)) == size(~V, m) : Nat} & ((@+q: String -> {mem(q, keys(~V, m2)) == Bool.and(Bool.not(str_eq(key, q)), mem(q, keys(~V, m))) : Bool}) & {nodup(keys(~V, m2)) == True{} : Bool}))))# Equivalent_Keysdef Equivalent_Keys.key_refl(+a: String) -> Type: {str_eq(a, a) == True{} : Bool}# Equivalent_Keysdef Equivalent_Keys.key_sym(+a: String, +b: String) -> Type: {str_eq(a, b) == str_eq(b, a) : Bool}# Equivalent_Keysdef Equivalent_Keys.key_trans(+a: String, +b: String, +c: String, +hab: {str_eq(a, b) == True{} : Bool}, +hbc: {str_eq(b, c) == True{} : Bool}) -> Type: {str_eq(a, c) == True{} : Bool}# Equivalent_Keysdef Equivalent_Keys.key_same(+a: String, +b: String, +h: {str_eq(a, b) == True{} : Bool}) -> Type: {a == b : String}# Equivalent_Keysdef Equivalent_Keys.key_respect(~A: Data, ~f: String -> A, +a: String, +b: String, +h: {str_eq(a, b) == True{} : Bool}) -> Type: {f(a) == f(b) : A}# Include (729)def Include.set_post(~V: Data, ~m: List<&2, Entry<V>>, ~m2: List<&2, Entry<V>>, ~key: String, ~x: V, ~hp: (@+q: String -> {lookup(~V, m2, q) == lookup(~V, set(~V, m, key, x), q) : Maybe<&2, V>}) & {size(~V, m2) == size(~V, set(~V, m, key, x)) : Nat}, +hnd: {nodup(keys(~V, m2)) == True{} : Bool}, hk: @+hq0: {has(~V, m, key) == True{} : Bool} -> {keys(~V, m2) == keys(~V, m) : List<&2, String>}) -> Type: SetPost(~V, m, m2, key, x)# The queries are stated on what they return: `r` is the value the operation# produces on a map whose model is `m` (the proof package instantiates it with# the implementation's result).# Element (SPARKlib formal-hashed-maps.ads): Element (Container, Key) = Get (Model, Key)def Element.element_value(~V: Data, m: List<&2, Entry<V>>, +key: String, +x: V, +hl: {lookup(~V, m, key) == Some{x} : Maybe<&2, V>}, r: V) -> Type: {r == x : V}# Element without the key: get returns the caller's default (the Pre of# Element is Contains; here the absent case is defined, not excluded)def Element.element_default(~V: Data, m: List<&2, Entry<V>>, +key: String, +dflt: V, +hl: {lookup(~V, m, key) == None{} : Maybe<&2, V>}, r: V) -> Type: {r == dflt : V}# Contains: Contains (Container, Key) = Has_Key (Model, Key)def Contains.contains_value(~V: Data, m: List<&2, Entry<V>>, +key: String, r: Bool) -> Type: {r == is_some(~V, lookup(~V, m, key)) : Bool}# Length: Length (Container) = M.Length (Model)def Length.length_value(~V: Data, m: List<&2, Entry<V>>, +n: Nat) -> Type: {n == SC.length(String, keys(~V, m)) : Nat}# Length is a query: the map is returned unchangeddef Length.length_frame(~V: Data, a: H.HashMap<&2, V>, b: H.HashMap<&2, V>) -> Type: {b == a : H.HashMap<&2, V>}# Empty_Map: Is_Empty (Model), Length = 0, no key presentdef Empty_Map.new_model(~V: Data, m: List<&2, Entry<V>>) -> Type: {m == Nil{} : List<&2, Entry<V>>}def Empty_Map.new_length(~V: Data, m: List<&2, Entry<V>>) -> Type: {size(~V, m) == 0n : Nat}def Empty_Map.new_absent(~V: Data, m: List<&2, Entry<V>>, +key: String) -> Type: {lookup(~V, m, key) == None{} : Maybe<&2, V>}