pub struct HashSetWithView<Key>{ /* private fields */ }Expand description
HashSetWithView is a trusted wrapper around std::collections::HashSet with View implemented for the type vstd::map::Set<<Key as View>::V>.
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<Key> HashSetWithView<Key>
impl<Key> HashSetWithView<Key>
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@ == Set::<<Key as View>::V>::empty(),Creates an empty HashSetWithView with capacity 0.
See obeys_key_model()
for information on use with primitive types and other types.
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
obeys_key_model::<Key>(),forall |k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,result@ == Set::<<Key as View>::V>::empty(),Creates an empty HashSetWithView 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 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 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 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 insert(&mut self, k: Key) -> result : bool
pub exec fn insert(&mut self, k: Key) -> 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: &Key) -> result : bool
pub exec fn remove(&mut self, k: &Key) -> 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: &Key) -> result : bool
pub exec fn contains(&self, k: &Key) -> 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: &Key) -> result : Option<&'a Key>
pub exec fn get<'a>(&'a self, k: &Key) -> result : Option<&'a Key>
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::<<Key as View>::V>::empty(),Clears all values from the set.
See Rust’s HashSet::clear() for implementation details.