consistency_model/
vec.rs

1use crate::SequentialSpec;
2
3/// An operation that can be invoked upon a [`Vec`], resulting in a
4/// [`VecRet`].
5#[derive(Clone, Debug, Hash, PartialEq)]
6#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
7pub enum VecOp<T> {
8    Push(T),
9    Pop,
10    Len,
11}
12
13/// A return value for a [`VecOp`] invoked upon a [`Vec`].
14#[derive(Clone, Debug, Hash, PartialEq)]
15#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
16pub enum VecRet<T> {
17    PushOk,
18    PopOk(Option<T>),
19    LenOk(usize),
20}
21
22impl<T> SequentialSpec for Vec<T>
23where
24    T: Clone + PartialEq,
25{
26    type Op = VecOp<T>;
27    type Ret = VecRet<T>;
28    fn invoke(&mut self, op: &Self::Op) -> Self::Ret {
29        match op {
30            VecOp::Push(v) => {
31                self.push(v.clone());
32                VecRet::PushOk
33            }
34            VecOp::Pop => VecRet::PopOk(self.pop()),
35            VecOp::Len => VecRet::LenOk(self.len()),
36        }
37    }
38    fn is_valid_step(&mut self, op: &Self::Op, ret: &Self::Ret) -> bool {
39        // Override to avoid unnecessary `clone` on `Pop`/`Len`.
40        match (op, ret) {
41            (VecOp::Push(v), VecRet::PushOk) => {
42                self.push(v.clone());
43                true
44            }
45            (VecOp::Pop, VecRet::PopOk(v)) => &self.pop() == v,
46            (VecOp::Len, VecRet::LenOk(l)) => &self.len() == l,
47            _ => false,
48        }
49    }
50}
51
52#[cfg(test)]
53mod test {
54    use super::*;
55
56    #[test]
57    fn models_expected_semantics() {
58        let mut v = vec!['A'];
59        assert_eq!(v.invoke(&VecOp::Len), VecRet::LenOk(1));
60        assert_eq!(v.invoke(&VecOp::Push('B')), VecRet::PushOk);
61        assert_eq!(v.invoke(&VecOp::Len), VecRet::LenOk(2));
62        assert_eq!(v.invoke(&VecOp::Pop), VecRet::PopOk(Some('B')));
63        assert_eq!(v.invoke(&VecOp::Len), VecRet::LenOk(1));
64        assert_eq!(v.invoke(&VecOp::Pop), VecRet::PopOk(Some('A')));
65        assert_eq!(v.invoke(&VecOp::Len), VecRet::LenOk(0));
66        assert_eq!(v.invoke(&VecOp::Pop), VecRet::PopOk(None));
67        assert_eq!(v.invoke(&VecOp::Len), VecRet::LenOk(0));
68    }
69
70    #[test]
71    fn accepts_valid_histories() {
72        assert!(Vec::<isize>::new().is_valid_history(vec![]));
73        assert!(Vec::new().is_valid_history(vec![
74            (VecOp::Push(10), VecRet::PushOk),
75            (VecOp::Push(20), VecRet::PushOk),
76            (VecOp::Len, VecRet::LenOk(2)),
77            (VecOp::Pop, VecRet::PopOk(Some(20))),
78            (VecOp::Len, VecRet::LenOk(1)),
79            (VecOp::Pop, VecRet::PopOk(Some(10))),
80            (VecOp::Len, VecRet::LenOk(0)),
81            (VecOp::Pop, VecRet::PopOk(None)),
82        ]));
83    }
84
85    #[test]
86    fn rejects_invalid_histories() {
87        assert!(!Vec::new().is_valid_history(vec![
88            (VecOp::Push(10), VecRet::PushOk),
89            (VecOp::Push(20), VecRet::PushOk),
90            (VecOp::Len, VecRet::LenOk(1)),
91            (VecOp::Push(30), VecRet::PushOk),
92        ]));
93        assert!(!Vec::new().is_valid_history(vec![
94            (VecOp::Push(10), VecRet::PushOk),
95            (VecOp::Push(20), VecRet::PushOk),
96            (VecOp::Pop, VecRet::PopOk(Some(10))),
97        ]));
98    }
99}
consistency_model/vec.rs

consistency_model/
vec.rs
