cdll/
invariants.rs

1#![allow(dead_code)]
2//! This module is used to documents the invariants that are meant to be
3//! preserved in this crate.
4
5/// If a [`CircularList<T>`](`crate::CircularList<T>`) is empty,
6/// its `head` (which is a [`ListHead<T>`](`crate::head::ListHead<T>`)) is
7/// null, otherwise it is a valid pointer that one can safely dereference.
8pub const INVARIANT_1: () = ();
9
10/// The `length` attribute of a [`CircularList<T>`](`crate::CircularList<T>`)
11/// is updated each time an element is added to the list or removed from it.
12pub const INVARIANT_2: () = ();
13
14/// Within a [`ListHead<T>`](`crate::head::ListHead<T>`):
15/// * The `next` and `prev` pointers are always valid
16/// * Following the `next` field recursively must always end up to the original `Self`
17/// * Following the `prev` field recursively must give the exact reverse path as the `next` one
18pub const INVARIANT_3: () = ();
19
20/// The `current` attribute of a [`Cursor<T>`](`crate::Cursor<T>`) is a valid pointer.
21pub const INVARIANT_4: () = ();
22
23/// Within a [`DoubleCursor<T>`](`crate::DoubleCursor<T>`):
24/// * `a` and `b` are always valid pointers
25/// * The `idx_a` and `idx_b` are always equal to the number of (forward) steps between the
26/// head and the position of `a` and `b` respectively
27pub const INVARIANT_5: () = ();
cdll/invariants.rs

cdll/
invariants.rs
