Trait Update 

pub trait Update<R: RA> {
    type Choice;

    // Required methods
    fn premise(self, from: R) -> bool;
    fn update(self, from: R, ch: Self::Choice) -> R;
    fn frame_preserving(self, from: R, frame: R) -> Self::Choice;
}

Perform an update on a resource.

This is used by Resource::update to specify how to update a resource.

Required Associated Types

type Choice

If the update is non-deterministic, it will pick a choice of this type for the update.

Required Methods

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

The premise of the update.

This must be true for the resource before applying the update.

logic

fn update(self, from: R, ch: Self::Choice) -> R

The actual update performed.

The content of the resource before the update is from. The update will also choose some element ch of Choice to make the update with. The return value will be the content of the resource after the update.

logic

requires

self.premise(from)

fn frame_preserving(self, from: R, frame: R) -> Self::Choice

Frame preservation.

This is a lemma that must be proven by implementors to ensure that the update is consistent.

It states that for any valid composition of self with some frame resource, we can find a Choice that, when applying the corresponding update, is still a valid composition with frame.

logic

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

Implementations on Foreign Types

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

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

logic(open, inline)

self.0.premise(from.0) && self.1.premise(from.1)

fn update(self, from: (R1, R2), ch: (U1::Choice, U2::Choice)) -> (R1, R2)

logic(open, inline)

self.0.update(from.0, ch.0), self.1.update(from.1, ch.1)

requires

self.premise(from)

fn frame_preserving(self, from: (R1, R2), frame: (R1, R2)) -> Self::Choice

logic

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = (<U1 as Update<R1>>::Choice, <U2 as Update<R2>>::Choice)

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

Apply no update.

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

logic(open, inline)

true

fn update(self, from: R, _: ()) -> R

logic(open, inline)

from

fn frame_preserving(self, from: R, frame: R)

logic

requires

from.op(frame) != None

ensures

from.op(frame) != None

type Choice = ()

Implementors

impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U>

type Choice = <U as Update<R1>>::Choice

impl<R: RA> Update<R> for Snapshot<R>

Apply a ‘raw’ update.

This changes the state of the resource from one value to another. The premise of this change is that no existing composition with the resource is invalidated.

type Choice = ()

impl<R: RA, Choice> Update<R> for Snapshot<Mapping<Choice, R>>

Apply a ‘raw’ non-deterministic update.

This changes the state of the resource to one of the values of the mapping, non-deterministically.

type Choice = Choice

impl<R: RA, U: Update<R>> Update<Option<R>> for OptionUpdate<U>

type Choice = <U as Update<R>>::Choice

impl<R: RA, U: Update<R>, V: RA> Update<Sum<V, R>> for SumUpdateR<U>

type Choice = <U as Update<R>>::Choice

impl<R: UnitRA, U: LocalUpdate<R>> Update<View<AuthViewRel<R>>> for AuthUpdate<U>

type Choice = ()

impl<R: ViewRel> Update<View<R>> for ViewUpdateInsert<R>

type Choice = ()

impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R>

type Choice = ()

impl<R: ViewRel, Choice> Update<View<R>> for ViewUpdate<R, Choice>

type Choice = Choice

impl<T> Update<Excl<T>> for ExclUpdate<T>

type Choice = ()