Undroppable

vstd_extra::undroppable

Trait Undroppable 

Source 
pub trait Undroppable {
    type State;

    // Required methods
    spec fn constructor_requires(self, s: Self::State) -> bool;
    spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool;
    proof fn constructor_spec(self, tracked s: &mut Self::State);
}

Required Associated Types§

Source

type State

Required Methods§

Source

spec fn constructor_requires(self, s: Self::State) -> bool

Source

spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool

Source

proof fn constructor_spec(self, tracked s: &mut Self::State)

requires
self.constructor_requires(*old(s)),
ensures
self.constructor_ensures(*old(s), *s),

Implementors§