pub struct StringHashSet { /* private fields */ }
Expand description
StringHashSet
is a trusted wrapper around std::collections::HashSet<String>
with View
implemented for the type vstd::map::Set<Seq<char>>
.
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 HashSet
for details about its implementation.
If you are using std::collections::HashSet
directly, see ExHashSet
for information on the Verus specifications for this type.
Implementations§
Source§impl StringHashSet
impl StringHashSet
Sourcepub exec fn new() -> result : Self
pub exec fn new() -> result : Self
result@ == Set::<Seq<char>>::empty(),
Creates an empty StringHashSet
with capacity 0.
See Rust’s HashSet::new()
for implementation details.
Sourcepub exec fn with_capacity(capacity: usize) -> result : Self
pub exec fn with_capacity(capacity: usize) -> result : Self
result@ == Set::<Seq<char>>::empty(),
Creates an empty StringHashSet
with at least capacity for the specified number of elements.
See Rust’s HashSet::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 set.
See Rust’s HashSet::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 set 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 set.
Sourcepub exec fn insert(&mut self, k: String) -> result : bool
pub exec fn insert(&mut self, k: String) -> result : bool
self@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
Inserts the given value into the set. Returns true if the value was not previously in the set, false otherwise.
See Rust’s HashSet::insert()
for implementation details.
Sourcepub exec fn remove(&mut self, k: &str) -> result : bool
pub exec fn remove(&mut self, k: &str) -> result : bool
self@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
Removes the given value from the set. Returns true if the value was previously in the set, false otherwise.
See Rust’s HashSet::remove()
for implementation details.
Sourcepub exec fn contains(&self, k: &str) -> result : bool
pub exec fn contains(&self, k: &str) -> result : bool
result == self@.contains(k@),
Returns true if the set contains the given value.
See Rust’s HashSet::contains()
for implementation details.
Sourcepub exec fn get<'a>(&'a self, k: &str) -> result : Option<&'a String>
pub exec fn get<'a>(&'a self, k: &str) -> result : Option<&'a String>
match result {
Some(v) => self@.contains(k@) && v@ == k@,
None => !self@.contains(k@),
},
Returns a reference to the value in the set that is equal to the given value. If the value is not present in the set, returns None
.
See Rust’s HashSet::get()
for implementation details.
Sourcepub exec fn clear(&mut self)
pub exec fn clear(&mut self)
self@ == Set::<Seq<char>>::empty(),
Clears all values from the set.
See Rust’s HashSet::clear()
for implementation details.