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

logic(prophetic)

fn resolve_coherence(self)

logic(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

logic(open, prophetic, inline)

*self@ == ^self@

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

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

fn resolve(self) -> bool

logic(open)

true

fn resolve_coherence(self)

logic

ensures

self.resolve()

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

fn resolve(self) -> bool

logic(open)

true

fn resolve_coherence(self)

logic

ensures

self.resolve()

impl<I> Resolve for Cloned<I>

fn resolve(self) -> bool

logic(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Copied<I>

fn resolve(self) -> bool

logic(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Enumerate<I>

fn resolve(self) -> bool

logic(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Skip<I>

fn resolve(self) -> bool

logic(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<I> Resolve for Take<I>

fn resolve(self) -> bool

logic(open, prophetic, inline)

resolve(self.iter())

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

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

fn resolve(self) -> bool

logic(open, prophetic, inline)

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

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T> Resolve for [T]

fn resolve(self) -> bool

logic(open, prophetic, inline)

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

fn resolve_coherence(self)

logic(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

logic(open, prophetic, inline)

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

fn resolve_coherence(self)

logic(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

logic(open, prophetic, inline)

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

fn resolve_coherence(self)

logic(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

logic(open, prophetic, inline)

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

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

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

fn resolve(self) -> bool

logic(open, prophetic, inline)

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

fn resolve_coherence(self)

logic(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

logic(open, prophetic, inline)

true

fn resolve_coherence(self)

logic(prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

Implementors

impl<C: ?Sized + Container> Resolve for Perm<C>

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

impl<T> Resolve for Seq<T>

impl<T> Resolve for SeqIter<T>

impl<T> Resolve for FSet<T>

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