Trait ResourceInvariant 

pub trait ResourceInvariant<V> {
    type Constant;
    type Resource;

    // Required method
    spec fn inv(constant: Self::Constant, value: V, resource: Self::Resource) -> bool;
}

An invariant that relates a value to a tracked resource with a constant.

Required Associated Types

type Constant

Immutable ghost configuration fixed at creation time.

type Resource

A tracked resource associated with the value and transferred linearly between owners.

Required Methods

spec fn inv(constant: Self::Constant, value: V, resource: Self::Resource) -> bool

The relation that must hold between the value, constant, and tracked resource.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<V, T: SimpleResourceInvariant<V>> ResourceInvariant<V> for T

type Constant = ()

type Resource = <T as SimpleResourceInvariant<V>>::Resource