class HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE]

All features

Auxilliary class to implement HASHED_BIJECTIVE_DICTIONARY.

Direct parents

conformant parents

ANY_HASHED_BIJECTIVE_DICTIONARY_NODE

Summary

creation features

exported features

Details

make (v: V_, nv: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE], k: K_, nk: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE])

require

  • v /= Void
  • k /= Void

ensure

  • val = v
  • next_val = nv
  • key = k
  • next_key = nk

val: V_
key: K_
next_key: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE]

The forward link to the next key in case of hash-code clash.

next_val: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE]

The forward link to the next val in case of hash-code clash.

make (v: V_, nv: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE], k: K_, nk: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE])

require

  • v /= Void
  • k /= Void

ensure

  • val = v
  • next_val = nv
  • key = k
  • next_key = nk

set_val (v: V_)

ensure

  • val = v

set_next_val (nv: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE])

ensure

  • next_val = nv

set_key (k: K_)

ensure

  • key = k

set_next_key (nk: HASHED_BIJECTIVE_DICTIONARY_NODE [V_ -> HASHABLE, K_ -> HASHABLE])

ensure

  • next_key = nk

set_val_and_key (v: V_, k: K_)

ensure

  • val = v
  • key = k

Class invariant