Function vstd::pcm_lib::update_and_redistribute

source ·

pub proof fn update_and_redistribute<P: PCM>(tracked 
    r1: &mut Resource<P>,
tracked     r2: &mut Resource<P>,
    v1: P,
    v2: P
)

Expand description

requires

old(r1).loc() == old(r2).loc(),

frame_preserving_update(P::op(old(r1).value(), old(r2).value()), P::op(v1, v2)),

ensures

r1.loc() == r2.loc() == old(r1).loc(),

r1.value() == v1,

r2.value() == v2,

Update the values held by resources r1 and r2 such that their values’ combination is updated in a frame-preserving way (i.e., that combination must be updatable in a frame-preserving way to the combination of v1 and v2). The new value of r1 will be v1 and the new value of r2 will be v2.