Skip to main content

frame_preserving_update_opt

vstd::resource::relations

Function frame_preserving_update_opt 

Source 
pub open spec fn frame_preserving_update_opt<RA: ResourceAlgebra>(a: RA, b: RA) -> bool
Expand description
{
    forall |c| {
        Option::<RA>::op(Some(a), c).valid() ==> Option::<RA>::op(Some(b), c).valid()
    }
}

A frame preserving update with support for resource algebras. See frame_preserving_update for more details. The difference lies in the fact that for PCMs there is always a unit