Trait SequentialSpec

Source

pub trait SequentialSpec: Sized {
    type Op;
    type Ret: PartialEq;

    // Required method
    fn invoke(&mut self, op: &Self::Op) -> Self::Ret;

    // Provided methods
    fn is_valid_step(&mut self, op: &Self::Op, ret: &Self::Ret) -> bool { ... }
    fn is_valid_history(
        &mut self,
        ops: impl IntoIterator<Item = (Self::Op, Self::Ret)>,
    ) -> bool { ... }
}

Expand description

An implementation of this trait can serve as a sequential “reference object” (in the sense of an operational specification, not a Rust reference) against which to validate the operational semantics of a more complex system, such as a distributed system.

This library includes the following ConsistencyTesters for verifying that a concurrent system adheres to an expected consistency model:

Required Associated Types§

Source

type Op

The type of operators. Often an enum.

Source

type Ret: PartialEq

The type of values return by the operators. Often an enum or Option.

Required Methods§

Source

fn invoke(&mut self, op: &Self::Op) -> Self::Ret

Invokes an operation on this reference object.

Provided Methods§

Source

fn is_valid_step(&mut self, op: &Self::Op, ret: &Self::Ret) -> bool

Indicates whether invoking a specified operation might result in a specified return value. Includes a default implementation that calls invoke, but a manual implementation may be provided for efficiency purposes (e.g. to avoid a clone() call).

Source