Trait creusot_contracts::invariant::Invariant

pub trait Invariant {
    // Required method
    fn invariant(self) -> bool;
}

Required Methods

fn invariant(self) -> bool

logic(prophetic)

Implementations on Foreign Types

impl Invariant for !

fn invariant(self) -> bool

logic(prophetic)

false

impl<T> Invariant for [T]

fn invariant(self) -> bool

logic(prophetic)

pearlite! { inv(self@) }

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

fn invariant(self) -> bool

logic(prophetic)

pearlite! { inv(self@) }

impl<T: ?Sized> Invariant for &T

fn invariant(self) -> bool

logic(prophetic)

inv(*self)

impl<T: ?Sized> Invariant for &mut T

fn invariant(self) -> bool

logic(prophetic)

pearlite! { inv(*self) && inv(^self) }

Implementors

impl<I: Iterator> Invariant for Enumerate<I>

impl<I: Iterator, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> Invariant for MapInv<I, I::Item, F>

impl<I: Iterator, F: FnMut(&I::Item) -> bool> Invariant for Filter<I, F>

impl<K, V: ?Sized> Invariant for FMap<K, V>

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

impl<T: ?Sized> Invariant for FSet<T>

impl<T: ?Sized> Invariant for Seq<T>

impl<T: ?Sized> Invariant for PtrOwn<T>

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