Skip to main content

frame_preserving_update_nondeterministic_opt

vstd::resource::relations

Function frame_preserving_update_nondeterministic_opt 

Source 
pub open spec fn frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
    a: RA,
    bs: Set<RA>,
) -> bool
Expand description
{
    forall |c| {
        Option::<RA>::op(Some(a), c).valid()
            ==> exists |b| {
                #[trigger] bs.contains(b) && Option::<RA>::op(Some(b), c).valid()
            }
    }
}

A nondeterministic version of a frame_preserving_update_opt.