Function vstd::pcm_lib::validate_multiple

source · 
pub proof fn validate_multiple<P: PCM>(tracked 
    m: &mut Map<int, Resource<P>>,
    loc: int,
    values: Seq<P>
)
Expand description
requires
forall |i| 0 <= i < values.len() ==> old(m).dom().contains(i),
forall |i| {
    0 <= i < values.len() ==> old(m)[i].loc() == loc && old(m)[i].value() == values[i]
},
ensures
forall |i| 0 <= i < values.len() ==> m.dom().contains(i),
forall |i| 0 <= i < values.len() ==> m[i].loc() == loc && m[i].value() == values[i],
combine_values(values).valid(),

Validates that a given sequence of resources has values that combine to form a valid value. Although that sequence consists of mutable references, none of those resources change. (They change in the middle of the function, but are restored by the time it completes.) The sequence of resources is specified using the following input parameters:

m – a map from integers to resources, mapping 0 to the first resource, 1 to the second, etc.

loc – the loc() shared by all the resources in m

values – the sequence of resources