Struct vstd::map::Map

source · 
pub struct Map<K, V> { /* private fields */ }
Expand description

Map<K, V> is an abstract map type for specifications. To use a “map” in compiled code, use an exec type like HashMap (TODO) that has a Map<K, V> as its specification type.

An object map: Map<K, V> has a domain, a set of keys given by map.dom(), and a mapping for keys in the domain to values, given by map[key]. Alternatively, a map can be thought of as a set of (K, V) pairs where each key appears in at most entry.

In general, a map might be infinite. To work specifically with finite maps, see the self.finite() predicate.

Maps can be constructed in a few different ways:

  • Map::empty() constructs an empty map.
  • Map::new and Map::total construct a map given functions that specify its domain and the mapping from keys to values (a map comprehension).
  • The map! macro, to construct small maps of a fixed size.
  • By manipulating an existing map with Map::insert or Map::remove.

To prove that two maps are equal, it is usually easiest to use the extensionality operator =~=.

Implementations§

source§

impl<K, V> Map<K, V>

source

pub spec fn empty() -> Map<K, V>

An empty map.

source

pub open spec fn total(fv: impl Fn(K) -> V) -> Map<K, V>

{ Set::full().mk_map(fv) }

Gives a Map<K, V> whose domain contains every key, and maps each key to the value given by fv.

source

pub open spec fn new(fk: impl Fn(K) -> bool, fv: impl Fn(K) -> V) -> Map<K, V>

{ Set::new(fk).mk_map(fv) }

Gives a Map<K, V> whose domain is given by the boolean predicate on keys fk, and maps each key to the value given by fv.

source

pub spec fn dom(self) -> Set<K>

The domain of the map as a set.

source

pub spec fn index(self, key: K) -> V

recommends
self.dom().contains(key),

Gets the value that the given key key maps to. For keys not in the domain, the result is meaningless and arbitrary.

source

pub open spec fn spec_index(self, key: K) -> V

recommends
self.dom().contains(key),
{ self.index(key) }

[] operator, synonymous with index

source

pub spec fn insert(self, key: K, value: V) -> Map<K, V>

Inserts the given (key, value) pair into the map.

If the key is already present from the map, then its existing value is overwritten by the new value.

source

pub spec fn remove(self, key: K) -> Map<K, V>

Removes the given key and its associated value from the map.

If the key is already absent from the map, then the map is left unchanged.

source

pub open spec fn len(self) -> nat

{ self.dom().len() }

Returns the number of key-value pairs in the map

source

pub open spec fn ext_equal(self, m2: Map<K, V>) -> bool

👎Deprecated: use =~= or =~~= instead
{ self =~= m2 }

DEPRECATED: use =~= or =~~= instead. Returns true if the two maps are pointwise equal, i.e., they have the same domains and the corresponding values are equal for each key. This is equivalent to the maps being actually equal by axiom_map_ext_equal.

To prove that two maps are equal via extensionality, it may be easier to use the general-purpose =~= or =~~= or to use the assert_maps_equal! macro, rather than using .ext_equal directly.

source

pub proof fn tracked_empty() -> tracked out_v : Self

ensures
out_v == Map::<K, V>::empty(),
source

pub proof fn tracked_insert(tracked &mut self, key: K, tracked value: V)

ensures
*self == Map::insert(*old(self), key, value),
source

pub proof fn tracked_remove(tracked &mut self, key: K) -> tracked v : V

requires
old(self).dom().contains(key),
ensures
*self == Map::remove(*old(self), key),
v == old(self)[key],

todo fill in documentation

source

pub proof fn tracked_borrow(tracked &self, key: K) -> tracked v : &V

requires
self.dom().contains(key),
ensures
*v === self.index(key),
source

pub proof fn tracked_map_keys<J>(tracked old_map: Map<K, V>, key_map: Map<J, K>) -> tracked new_map : Map<J, V>

requires
forall |j| key_map.dom().contains(j) ==> old_map.dom().contains(key_map.index(j)),
forall |j1, j2| {
    !equal(j1, j2) && key_map.dom().contains(j1) && key_map.dom().contains(j2)
        ==> !equal(key_map.index(j1), key_map.index(j2))
},
ensures
forall |j| #[trigger] new_map.dom().contains(j) <==> key_map.dom().contains(j),
forall |j| {
    key_map.dom().contains(j)
        ==> new_map.dom().contains(j)
            && #[trigger] new_map.index(j) == old_map.index(key_map.index(j))
},
source

pub proof fn tracked_remove_keys(tracked &mut self, keys: Set<K>) -> tracked out_map : Map<K, V>

requires
keys.subset_of(old(self).dom()),
ensures
self == old(self).remove_keys(keys),
out_map == old(self).restrict(keys),
source

pub proof fn tracked_union_prefer_right(tracked &mut self, right: Self)

ensures
*self == old(self).union_prefer_right(right),
source§

impl<K, V> Map<K, V>

source

pub proof fn tracked_map_keys_in_place(&mut self, key_map: Map<K, K>)

requires
forall |j| key_map.dom().contains(j) ==> old(self).dom().contains(key_map.index(j)),
forall |j1, j2| {
    j1 != j2 && key_map.dom().contains(j1) && key_map.dom().contains(j2)
        ==> key_map.index(j1) != key_map.index(j2)
},
ensures
forall |j| #[trigger] self.dom().contains(j) == key_map.dom().contains(j),
forall |j| {
    key_map.dom().contains(j)
        ==> self.dom().contains(j)
            && #[trigger] self.index(j) == old(self).index(key_map.index(j))
},
source§

impl<K, V> Map<K, V>

source

pub open spec fn is_full(self) -> bool

{ self.dom().is_full() }

Is true if called by a “full” map, i.e., a map containing every element of type A.

source

pub open spec fn is_empty(self) -> b : bool

{ self.dom().is_empty() }

Is true if called by an “empty” map, i.e., a map containing no elements and has length 0

source

pub open spec fn contains_key(self, k: K) -> bool

{ self.dom().contains(k) }

Returns true if the key k is in the domain of self.

source

pub open spec fn contains_value(self, v: V) -> bool

{ exists |i: K| #[trigger] self.dom().contains(i) && self[i] == v }

Returns true if the value v is in the range of self.

source

pub open spec fn values(self) -> Set<V>

{ Set::<V>::new(|v: V| self.contains_value(v)) }

Returns the set of values in the map.

§Example
assert(
   map![1 => 10, 2 => 11].values() =~= set![10, 11]
);
source

pub open spec fn contains_pair(self, k: K, v: V) -> bool

{ self.dom().contains(k) && self[k] == v }

Returns true if the key k is in the domain of self, and it maps to the value v.

source

pub open spec fn submap_of(self, m2: Self) -> bool

{
    forall |k: K| {
        #[trigger] self.dom().contains(k)
            ==> #[trigger] m2.dom().contains(k) && self[k] == m2[k]
    }
}

Returns true if m1 is contained in m2, i.e., the domain of m1 is a subset of the domain of m2, and they agree on all values in m1.

§Example
assert(
   map![1 => 10, 2 => 11].le(map![1 => 10, 2 => 11, 3 => 12])
);
source

pub open spec fn spec_le(self, m2: Self) -> bool

{ self.submap_of(m2) }
source

pub open spec fn le(self, m2: Self) -> bool

👎Deprecated: use m1.submap_of(m2) or m1 <= m2 instead
{ self.submap_of(m2) }

Deprecated synonym for submap_of

source

pub open spec fn union_prefer_right(self, m2: Self) -> Self

{
    Self::new(
        |k: K| self.dom().contains(k) || m2.dom().contains(k),
        |k: K| if m2.dom().contains(k) { m2[k] } else { self[k] },
    )
}

Gives the union of two maps, defined as:

  • The domain is the union of the two input maps.
  • For a given key in both input maps, it maps to the same value that it maps to in the right map (m2).
  • For any other key in either input map (but not both), it maps to the same value as it does in that map.
§Example
assert(
   map![1 => 10, 2 => 11].union_prefer_right(map![1 => 20, 3 => 13])
   =~= map![1 => 20, 2 => 11, 3 => 13]);
source

pub open spec fn remove_keys(self, keys: Set<K>) -> Self

{ Self::new(|k: K| self.dom().contains(k) && !keys.contains(k), |k: K| self[k]) }

Removes the given keys and their associated values from the map.

Ignores any key in keys which is not in the domain of self.

§Example
assert(
   map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
   =~= map![1 => 10]);
source

pub open spec fn restrict(self, keys: Set<K>) -> Self

{ Self::new(|k: K| self.dom().contains(k) && keys.contains(k), |k: K| self[k]) }

Complement to remove_keys. Restricts the map to (key, value) pairs for keys that are in the given set; that is, it removes any keys not in the set.

§Example
assert(
   map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
   =~= map![2 => 11, 3 => 12]);
source

pub open spec fn is_equal_on_key(self, m2: Self, key: K) -> bool

{
    ||| (!self.dom().contains(key) && !m2.dom().contains(key))
    ||| (self.dom().contains(key) && m2.dom().contains(key) && self[key] == m2[key])

}

Returns true if and only if the given key maps to the same value or does not exist in self and m2.

source

pub open spec fn agrees(self, m2: Self) -> bool

{ forall |k| self.dom().contains(k) && m2.dom().contains(k) ==> self[k] == m2[k] }

Returns true if the two given maps agree on all keys that their domains share

source

pub open spec fn map_entries<W>(self, f: FnSpec<(K, V), W>) -> Map<K, W>

{ Map::new(|k: K| self.contains_key(k), |k: K| f(k, self[k])) }

Map a function f over all (k, v) pairs in self.

source

pub open spec fn map_values<W>(self, f: FnSpec<(V,), W>) -> Map<K, W>

{ Map::new(|k: K| self.contains_key(k), |k: K| f(self[k])) }

Map a function f over the values in self.

source

pub open spec fn is_injective(self) -> bool

{
    forall |x: K, y: K| {
        x != y && self.dom().contains(x) && self.dom().contains(y)
            ==> #[trigger] self[x] != #[trigger] self[y]
    }
}

Returns true if and only if a map is injective

source

pub open spec fn invert(self) -> Map<V, K>

{
    Map::<
        V,
        K,
    >::new(|v: V| self.contains_value(v), |v: V| choose |k: K| self.contains_pair(k, v))
}

Swaps map keys and values. Values are not required to be unique; no promises on which key is chosen on the intersection.

source

pub proof fn lemma_remove_key_len(self, key: K)

requires
self.dom().contains(key),
self.dom().finite(),
ensures
self.dom().len() == 1 + self.remove(key).dom().len(),

Removing a key from a map that previously contained that key decreases the map’s length by one

source

pub proof fn lemma_remove_equivalency(self, key: K)

ensures
self.remove(key).dom() == self.dom().remove(key),

The domain of a map after removing a key is equivalent to removing the key from the domain of the original map.

source

pub proof fn lemma_remove_keys_len(self, keys: Set<K>)

requires
forall |k: K| #[trigger] keys.contains(k) ==> self.contains_key(k),
keys.finite(),
self.dom().finite(),
ensures
self.remove_keys(keys).dom().len() == self.dom().len() - keys.len(),

Removing a set of n keys from a map that previously contained all n keys results in a domain of size n less than the original domain.

source

pub proof fn lemma_invert_is_injective(self)

ensures
self.invert().is_injective(),

The function invert results in an injective map

source§

impl Map<int, int>

source

pub open spec fn is_monotonic(self) -> bool

{
    forall |x: int, y: int| {
        self.dom().contains(x) && self.dom().contains(y) && x <= y
            ==> #[trigger] self[x] <= #[trigger] self[y]
    }
}

Returns true if a map is monotonic – that is, if the mapping between ordered sets preserves the regular <= ordering on integers.

source

pub open spec fn is_monotonic_from(self, start: int) -> bool

{
    forall |x: int, y: int| {
        self.dom().contains(x) && self.dom().contains(y) && start <= x <= y
            ==> #[trigger] self[x] <= #[trigger] self[y]
    }
}

Returns true if and only if a map is monotonic, only considering keys greater than or equal to start

Auto Trait Implementations§

§

impl<K, V> Freeze for Map<K, V>

§

impl<K, V> RefUnwindSafe for Map<K, V>
where K: RefUnwindSafe, V: RefUnwindSafe,

§

impl<K, V> Send for Map<K, V>
where K: Send, V: Send,

§

impl<K, V> Sync for Map<K, V>
where K: Sync, V: Sync,

§

impl<K, V> Unpin for Map<K, V>
where K: Unpin, V: Unpin,

§

impl<K, V> UnwindSafe for Map<K, V>
where K: UnwindSafe, V: UnwindSafe,

Blanket Implementations§

source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.