Trait todc_utils::specifications::Specification

source ·

pub trait Specification {
    type State: Clone + Eq + Hash + Debug;
    type Operation: Clone + Debug;

    // Required methods
    fn init() -> Self::State;
    fn apply(op: &Self::Operation, state: &Self::State) -> (bool, Self::State);
}

Expand description

A (sequential) specification of an object.

This trait defines how operations performed on the object affect its state.

Examples

Consider the following specification for a register that stores a single u32 value. Initially, the register contains the value 0.

use todc_utils::Specification;

#[derive(Copy, Clone, Debug)]
enum RegisterOp {
    Read(u32),
    Write(u32),
}

use RegisterOp::{Read, Write};

struct RegisterSpec;

impl Specification for RegisterSpec {
    type State = u32;
    type Operation = RegisterOp;
     
    fn init() -> Self::State {
        0
    }

    fn apply(operation: &Self::Operation, state: &Self::State) -> (bool, Self::State) {
        match operation {
            Read(value) => (value == state, *state),
            Write(value) => (true, *value),
        }
    }
}

A Write operation is always valid, as is a Read operation that returns the value of the most-recent write.

let (is_valid, new_state) = RegisterSpec::apply(&Write(1), &RegisterSpec::init());
assert!(is_valid);
assert_eq!(new_state, 1);

let (is_valid, new_state) = RegisterSpec::apply(&Read(1), &new_state);
assert!(is_valid);
assert_eq!(new_state, 1);

On the other hand, a Read operation that returns a different value to the one currently stored in the register is not valid.

let (_, new_state) = RegisterSpec::apply(&Write(1), &RegisterSpec::init());
let (is_valid, _) = RegisterSpec::apply(&Read(42), &new_state);
assert!(!is_valid);