pub struct StringHashMap<Value> { /* private fields */ }Expand description
StringHashMap is a trusted wrapper around std::collections::HashMap<String, Value> with View implemented for the type vstd::map::Map<Seq<char>, Value>.
This type was created for ease of use with String as it uses &str instead of &String for methods that require shared references.
Also, it assumes that obeys_key_model::<String>() holds.
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<Value> StringHashMap<Value>
impl<Value> StringHashMap<Value>
Sourcepub exec fn new() -> result : Self
pub exec fn new() -> result : Self
result@ == Map::<Seq<char>, Value>::empty(),Creates an empty StringHashMap with a capacity of 0.
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
result@ == Map::<Seq<char>, Value>::empty(),Creates an empty StringHashMap with at least capacity for the specified number of elements.
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: String, v: Value)
pub exec fn insert(&mut self, k: String, 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: &str)
pub exec fn remove(&mut self, k: &str)
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: &str) -> result : bool
pub exec fn contains_key(&self, k: &str) -> 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: &str) -> result : Option<&'a Value>
pub exec fn get<'a>(&'a self, k: &str) -> 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::<Seq<char>, 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.