Struct Authority 

pub struct Authority<K, V>(/* private fields */);

Wrapper around a Resource, that allows to agree on the values of a FMap.

This is the authoritative version

Implementations

impl<K, V> Authority<K, V>

pub fn id(self) -> Id

Id of the underlying Resource.

pub fn new() -> Ghost<Self>

Create a new, empty authoritative map.

terminates

ghost

ensures

result@ == FMap::empty()

pub fn insert(&mut self, k: Snapshot<K>, v: Snapshot<V>) -> Fragment<K, V>

Insert a new element in the authoritative map and return the corresponding fragment.

requires

!self@.contains(*k)

ensures

(^self)@ == self@.insert(*k, *v)

ensures

(^self).id() == self.id()

ensures

result@ == (*k, *v)

ensures

result.id() == self.id()

terminates

ghost

pub fn contains(&self, frag: &Fragment<K, V>)

Asserts that the fragment represented by frag is contained in self.

requires

self.id() == frag.id()

ensures

self@.get(frag@.0) == Some(frag@.1)

terminates

ghost

Trait Implementations

impl<K, V> Invariant for Authority<K, V>

fn invariant(self) -> bool

impl<K, V> View for Authority<K, V>

fn view(self) -> FMap<K, V>

Get the authoritative version of the map.

type ViewTy = FMap<K, V>