pub struct HashMapWithView<Key, Value>{ /* private fields */ }Expand description
HashMapWithView is a trusted wrapper around std::collections::HashMap with View implemented for the type vstd::map::Map<<Key as View>::V, Value>.
See the Rust documentation for HashMap
for details about its implementation.
If you are using std::collections::HashMap directly, see ExHashMap
for information on the Verus specifications for this type.
Implementations§
Source§impl<Key, Value> HashMapWithView<Key, Value>
impl<Key, Value> HashMapWithView<Key, Value>
Sourcepub exec fn new() -> result : Self
pub exec fn new() -> result : Self
obeys_key_model::<Key>(),forall |k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,result@ == Map::<<Key as View>::V, Value>::empty(),Creates an empty HashMapWithView with a capacity of 0.
See obeys_key_model()
for information on use with primitive types and other types.
See Rust’s HashMap::new() for implementation details.
Sourcepub exec fn with_capacity(capacity: usize) -> result : Self
pub exec fn with_capacity(capacity: usize) -> result : Self
obeys_key_model::<Key>(),forall |k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,result@ == Map::<<Key as View>::V, Value>::empty(),Creates an empty HashMapWithView with at least capacity for the specified number of elements.
See obeys_key_model()
for information on use with primitive types and other types.
See Rust’s HashMap::with_capacity() for implementation details.
Sourcepub exec fn reserve(&mut self, additional: usize)
pub exec fn reserve(&mut self, additional: usize)
self@ == old(self)@,Reserves capacity for at least additional number of elements in the map.
See Rust’s HashMap::reserve() for implementation details.
Sourcepub exec fn is_empty(&self) -> result : bool
pub exec fn is_empty(&self) -> result : bool
result == self@.is_empty(),Returns true if the map is empty.
Sourcepub exec fn len(&self) -> result : usize
pub exec fn len(&self) -> result : usize
result == self@.len(),Returns the number of elements in the map.
Sourcepub exec fn insert(&mut self, k: Key, v: Value)
pub exec fn insert(&mut self, k: Key, v: Value)
self@ == old(self)@.insert(k@, v),Inserts the given key and value in the map.
See Rust’s HashMap::insert() for implementation details.
Sourcepub exec fn remove(&mut self, k: &Key)
pub exec fn remove(&mut self, k: &Key)
self@ == old(self)@.remove(k@),Removes the given key from the map. If the key is not present in the map, the map is unmodified.
See Rust’s HashMap::remove() for implementation details.
Sourcepub exec fn contains_key(&self, k: &Key) -> result : bool
pub exec fn contains_key(&self, k: &Key) -> result : bool
result == self@.contains_key(k@),Returns true if the map contains the given key.
See Rust’s HashMap::contains_key() for implementation details.
Sourcepub exec fn get<'a>(&'a self, k: &Key) -> result : Option<&'a Value>
pub exec fn get<'a>(&'a self, k: &Key) -> result : Option<&'a Value>
match result {
Some(v) => self@.contains_key(k@) && *v == self@[k@],
None => !self@.contains_key(k@),
},Returns a reference to the value corresponding to the given key in the map. If the key is not present in the map, returns None.
See Rust’s HashMap::get() for implementation details.
Sourcepub exec fn clear(&mut self)
pub exec fn clear(&mut self)
self@ == Map::<<Key as View>::V, Value>::empty(),Clears all key-value pairs in the map. Retains the allocated memory for reuse.
See Rust’s HashMap::clear() for implementation details.
Sourcepub exec fn union_prefer_right(&mut self, other: Self)
pub exec fn union_prefer_right(&mut self, other: Self)
self@ == old(self)@.union_prefer_right(other@),Returns the union of the two maps. If a key is present in both maps, then the value in the right map (other) is retained.