Continuation

vest_lib::regular::sequence

Trait Continuation 

Source 
pub trait Continuation<Input> {
    type Output;

    // Required methods
    exec fn apply(&self, i: Input) -> o : Self::Output;
    spec fn requires(&self, i: Input) -> bool;
    spec fn ensures(&self, i: Input, o: Self::Output) -> bool;
}
Expand description

Use this Continuation trait instead of Fn(Input) -> Output to avoid unsupported Verus features

Required Associated Types§

Source

type Output

Output type of the continuation

Required Methods§

Source

exec fn apply(&self, i: Input) -> o : Self::Output

requires
self.requires(i),
ensures
self.ensures(i, o),

The actual continuation function

Source

spec fn requires(&self, i: Input) -> bool

The precondition of the continuation

Source

spec fn ensures(&self, i: Input, o: Self::Output) -> bool

The postcondition of the continuation

Implementors§