Trait LocalUpdate 

pub trait LocalUpdate<R: RA>: Sized {
    // Required methods
    fn premise(self, from_auth: R, from_frag: R) -> bool;
    fn update(self, from_auth: R, from_frag: R) -> (R, R);
    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>);
}

Required Methods

fn premise(self, from_auth: R, from_frag: R) -> bool

logic

fn update(self, from_auth: R, from_frag: R) -> (R, R)

logic

fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>)

logic

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<R1: RA, R2: RA, U1: LocalUpdate<R1>, U2: LocalUpdate<R2>> LocalUpdate<(R1, R2)> for (U1, U2)

fn premise(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> bool

logic(open, inline)

self.0.premise(from_auth.0, from_frag.0) && self.1.premise(from_auth.1, from_frag.1)

fn update( self, from_auth: (R1, R2), from_frag: (R1, R2), ) -> ((R1, R2), (R1, R2))

logic(open, inline)

let (to_auth0, to_frag0) = self.0.update(from_auth.0, from_frag.0);
let (to_auth1, to_frag1) = self.1.update(from_auth.1, from_frag.1);
((to_auth0, to_auth1), (to_frag0, to_frag1))

fn frame_preserving( self, from_auth: (R1, R2), from_frag: (R1, R2), frame: Option<(R1, R2)>, )

logic

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

impl<R: RA> LocalUpdate<R> for ()

fn premise(self, _: R, _: R) -> bool

logic(open, inline)

true

fn update(self, from_auth: R, from_frag: R) -> (R, R)

logic(open, inline)

from_auth, from_frag

fn frame_preserving(self, auth: R, frag: R, frame: Option<R>)

logic

requires

Some(frag).op(frame) == Some(Some(auth))

ensures

Some(frag).op(frame) == Some(Some(auth))

Implementors

impl LocalUpdate<Int> for Int

impl<K, V: RA> LocalUpdate<FMap<K, V>> for FMapInsertLocalUpdate<K, V>

impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U>

impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U>

impl<R: RA> LocalUpdate<R> for Snapshot<(R, R)>

impl<R: RA, U: LocalUpdate<R>> LocalUpdate<Option<R>> for OptionLocalUpdate<U>