~/bend-docscommunity

proofs/containers/hash_table/new.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/new.bend as New

5 imports
import Base
import ../../lib/array.bend as AR
import ../../../spec/containers/hash_table.bend as S
import ../../../src/containers/hash_table.bend as H
import ./state.bend as ST

Templates

template empty source · line 9 · raw

@-V:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V>

template new_ok source · line 13 · raw

@-V:Data -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.new(&2, V) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, empty(V)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, empty(V)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, empty(V)) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>}))

THEOREM: new is the shadow of the empty specification map