Verifying Data Structures

Data structures are the backbone of software. A stack that silently drops elements, a queue whose ordering breaks, or a binary tree that loses its search property after deletion — these are bugs that unit tests rarely catch exhaustively. Deppy lets you verify that your data structures maintain their invariants across all operations, for all inputs, without modifying the Python code itself. This chapter covers dataclasses, class invariants, method contracts, inheritance verification, and culminates with a fully verified binary search tree.

Dataclass Verification

Python's @dataclass decorator creates well-behaved classes automatically — generating __init__, __repr__, __eq__, and more. Deppy understands dataclasses natively and lets you attach invariants at the class level with @guarantee.

from __future__ import annotations
from dataclasses import dataclass

@dataclass
class Point:
    x: float
    y: float
    radius: float

This is ordinary Python. In a Deppy sidecar file, we add the invariant that the point lies within a circle of the given radius:

# point_spec.deppy
@guarantee("self.x ** 2 + self.y ** 2 <= self.radius ** 2")
class Point: ...

Deppy verifies that every construction of a Point satisfies this invariant — writing Point(10, 10, 5) triggers a violation because 10² + 10² = 200 > 25 = 5². Here is another dataclass where the low bound never exceeds the high bound:

@dataclass
class Range:
    lo: int
    hi: int

# range_spec.deppy
@guarantee("self.lo <= self.hi")
class Range: ...

Class Invariants with @invariant

While @guarantee works well for simple dataclasses, mutable classes with methods need a stronger contract: @invariant. An invariant must hold after __init__ completes and before and after every public method call. Deppy checks this automatically.

class BoundedList:
    def __init__(self, capacity: int) -> None:
        self.capacity = capacity
        self.items: list[int] = []

    def add(self, x: int) -> None:
        if len(self.items) < self.capacity:
            self.items.append(x)

    def size(self) -> int:
        return len(self.items)

# bounded_list_spec.deppy
@invariant("len(self.items) <= self.capacity")
class BoundedList: ...

Deppy proves that len(self.items) ≤ self.capacity is established by __init__ and preserved by add — the guard is exactly what Z3 needs.

Method Contracts (Pre/Postconditions)

Individual methods can have their own contracts on top of the class invariant. Use @assume for preconditions and @guarantee for postconditions. Inside a postcondition, the old_ prefix refers to the value of an expression before the method was called — Deppy snapshots these at method entry.

# stack_spec.deppy
@invariant("len(self._items) >= 0")
class Stack:
    @guarantee("self.size() == old_size + 1")
    def push(self, x): ...

    @assume("not self.is_empty()")
    @guarantee("self.size() == old_size - 1")
    def pop(self): ...

    @assume("not self.is_empty()")
    def peek(self): ...

The old_size variable is bound to self.size() evaluated at method entry, then checked against the post-state.

Verified Stack — Complete Example

Here is a complete, verified stack. First the pure Python code:

from __future__ import annotations
from typing import Generic, TypeVar
T = TypeVar('T')

class Stack(Generic[T]):
    def __init__(self) -> None:
        self._items: list[T] = []

    def push(self, value: T) -> None:
        self._items.append(value)

    def pop(self) -> T:
        return self._items.pop()

    def peek(self) -> T:
        return self._items[-1]

    def is_empty(self) -> bool:
        return len(self._items) == 0

    def size(self) -> int:
        return len(self._items)

The sidecar specification adds contracts:

# stack_spec.deppy — sidecar proof for Stack
@invariant("len(self._items) >= 0")
class Stack:
    @guarantee("not self.is_empty()")
    @guarantee("self.size() == old_size + 1")
    @guarantee("self.peek() == value")
    def push(self, value): ...

    @assume("not self.is_empty()")
    @guarantee("self.size() == old_size - 1")
    @guarantee("result == old_peek")
    def pop(self): ...

    @assume("not self.is_empty()")
    @guarantee("result == self._items[-1]")
    def peek(self): ...

    @guarantee("result == (self.size() == 0)")
    def is_empty(self): ...

Running python -m deppy.pipeline.run_verify stack.py produces:

  ✓ Stack.__init__     — invariant established
  ✓ Stack.push         — 3 guarantees proved (Z3, 0.04s)
  ✓ Stack.pop          — 2 guarantees proved (Z3, 0.06s)
  ✓ Stack.peek         — 1 guarantee proved  (Z3, 0.01s)
  ✓ Stack.is_empty     — 1 guarantee proved  (Z3, 0.01s)
  ✓ Stack              — invariant preserved by all methods
  ────────────────────────────────────────────
  6/6 obligations discharged  ·  Z3_VERIFIED

Verified Queue

A classic two-list queue uses a front list for dequeuing and a back list for enqueuing, reversing back into front when needed. The key invariant: if front is empty then back must also be empty.

from __future__ import annotations
from typing import Generic, TypeVar
T = TypeVar('T')

class Queue(Generic[T]):
    def __init__(self) -> None:
        self._front: list[T] = []
        self._back: list[T] = []

    def _transfer(self) -> None:
        if not self._front:
            self._front = self._back[::-1]
            self._back = []

    def enqueue(self, value: T) -> None:
        self._back.append(value)
        self._transfer()

    def dequeue(self) -> T:
        self._transfer()
        return self._front.pop()

    def is_empty(self) -> bool:
        return not self._front and not self._back

# queue_spec.deppy
@invariant("not self._front implies not self._back")
class Queue:
    @guarantee("not self.is_empty()")
    def enqueue(self, value): ...

    @assume("not self.is_empty()")
    def dequeue(self): ...

Deppy verifies that enqueue preserves the invariant and that dequeue is safe given its precondition.

Inheritance and Liskov Substitution

If class B extends class A, then B must satisfy all of A's invariants — the Liskov substitution principle (LSP). Deppy verifies LSP automatically.

class SortedList(list[int]):
    def add(self, value: int) -> None:
        for i, item in enumerate(self):
            if value <= item:
                self.insert(i, value)
                return
        self.append(value)

# sorted_list_spec.deppy
@invariant("all(self[i] <= self[i+1] for i in range(len(self)-1))")
class SortedList:
    @guarantee("value in self")
    def add(self, value): ...

When LSP is violated — say someone overrides append without maintaining sorted order — Deppy catches it:

class BrokenSortedList(SortedList):
    def append(self, value: int) -> None:
        # Appends without checking order — breaks invariant!
        super().append(value)

  ✗ BrokenSortedList.append — invariant violated
    Counterexample: self = [1, 3, 5], value = 2
    After append: [1, 3, 5, 2]  — not sorted
    LSP violation: BrokenSortedList cannot substitute SortedList

Verified Binary Search Tree

Binary search trees are a classic test of verification tools. The BST invariant — all left descendants are smaller, all right descendants are larger — must be preserved across insertions and deletions. Here is a complete implementation:

from __future__ import annotations
from typing import Optional

class Node:
    def __init__(self, value: int) -> None:
        self.value, self.left, self.right = value, None, None

class BST:
    def __init__(self) -> None:
        self.root: Optional[Node] = None

    def _is_bst(self, node: Optional[Node], lo: float, hi: float) -> bool:
        if node is None: return True
        if not (lo < node.value < hi): return False
        return (self._is_bst(node.left, lo, node.value)
                and self._is_bst(node.right, node.value, hi))

    def _insert(self, node: Optional[Node], value: int) -> Node:
        if node is None: return Node(value)
        if value < node.value:   node.left = self._insert(node.left, value)
        elif value > node.value: node.right = self._insert(node.right, value)
        return node

    def insert(self, value: int) -> None:
        self.root = self._insert(self.root, value)

    def search(self, value: int, node: Optional[Node] = None) -> bool:
        n = node if node is not None else self.root
        if n is None: return False
        if value == n.value: return True
        return self.search(value, n.left if value < n.value else n.right)

    def _find_min(self, node: Node) -> int:
        while node.left is not None: node = node.left
        return node.value

    def _delete(self, node: Optional[Node], value: int) -> Optional[Node]:
        if node is None: return None
        if value < node.value:
            node.left = self._delete(node.left, value)
        elif value > node.value:
            node.right = self._delete(node.right, value)
        else:
            if node.left is None:  return node.right
            if node.right is None: return node.left
            successor = self._find_min(node.right)
            node.value = successor
            node.right = self._delete(node.right, successor)
        return node

    def delete(self, value: int) -> None:
        self.root = self._delete(self.root, value)

The sidecar proof specifies the BST invariant and method contracts:

# bst_spec.deppy — sidecar proof for BST
@invariant("self._is_bst(self.root, float('-inf'), float('inf'))")
class BST:
    @guarantee("self.search(value)")
    def insert(self, value): ...

    @guarantee("result implies self._contains(self.root, value)")
    @guarantee("not result implies not self._contains(self.root, value)")
    def search(self, value): ...

    @guarantee("not self.search(value)")
    def delete(self, value): ...

Verification proceeds structurally — Deppy assumes the invariant on entry (inductive hypothesis), symbolically executes the method body, then proves the invariant and all guarantees hold on exit:

  ✓ BST.__init__       — invariant established (trivial: root is None)
  ✓ BST.insert         — invariant preserved, guarantee proved
                         (structural induction on tree depth, Z3, 0.23s)
  ✓ BST.search         — 2 guarantees proved (Z3, 0.08s)
  ✓ BST.delete         — invariant preserved, guarantee proved
                         (case split: 0/1/2 children, Z3, 0.41s)
  ────────────────────────────────────────────
  4/4 obligations discharged  ·  Z3_VERIFIED

The delete case is the most complex — Deppy reasons about the in-order successor replacement via a case split over the three deletion scenarios (leaf, one child, two children).

Practical Notes

s = Stack()
alias = s
alias._items.append(42)  # bypasses Stack.push — invariant unchecked!

Exercise

Next Steps

You now know how to verify data structures with class invariants, method contracts, and inheritance checks. In the next chapter we tackle termination — proving that recursive and iterative algorithms always finish.