Trait Resolve 

pub trait Resolve {
    // Required methods
    fn resolve(self) -> bool;
    fn resolve_coherence(self);
}

The trait Resolve makes it possible to expose to clients a custom resolve assertion for opaque types.

For example, if a library defines a notion of finite mapping, it does not exposes the internal representation of the finite mapping data structure. Hence, the resolve predicate above wil be completely opaque for clients. This library should implement the Resolve trait in order to provide to the client a definition it can use. E.g., Resolve::resolve states that any element of the mapping is resolved.

Required Methods

fn resolve(self) -> bool

(prophetic)

fn resolve_coherence(self)

(prophetic)

requires

inv(self)

requires

structural_resolve(self)

ensures

self.resolve()

Implementations on Foreign Types

impl<'a, T> Resolve for IterMut<'a, T>

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { *self@ == ^self@ }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<'a, T: ?Sized> Resolve for &'a T

fn resolve(self) -> bool

(open)

true

fn resolve_coherence(self)

ensures

self.resolve()

impl<'a, T: ?Sized> Resolve for &'a mut T

fn resolve(self) -> bool

(open)

true

fn resolve_coherence(self)

ensures

self.resolve()

impl<I> Resolve for Cloned<I>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Copied<I>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Enumerate<I>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Skip<I>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Take<I>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I, F> Resolve for Map<I, F>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.iter()) && resolve(self.func())

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T> Resolve for [T]

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T, A: Allocator> Resolve for VecDeque<T, A>

Available on crate feature nightly only.

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T, A: Allocator> Resolve for IntoIter<T, A>

Available on crate feature nightly only.

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self@[i]) }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T, A: Allocator> Resolve for Vec<T, A>

Available on crate feature nightly only.

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T, const N: usize> Resolve for [T; N]

fn resolve(self) -> bool

(open, prophetic, inline)

pearlite! { forall<i: Int> 0 <= i && i < N@ ==> resolve(self@[i]) }

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T: ?Sized, A: Allocator> Resolve for Box<T, A>

Available on crate feature nightly only.

fn resolve(self) -> bool

(open, prophetic, inline)

true

fn resolve_coherence(self)

(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

Implementors

impl<K, V> Resolve for FMap<K, V>

impl<T> Resolve for FSet<T>

impl<T> Resolve for Seq<T>

impl<T> Resolve for SeqIter<T>

impl<T: InhabitedInvariant> Resolve for Subset<T>

impl<T: ?Sized> Resolve for PermCellOwn<T>