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.