"We introduce the syntax \mathit{stack}, \mathit{empty}, \mathit{push}, \mathit{pop}, and \mathit{top}." The axioms: \mathit{empty} : \mathit{stack}, \mathit{push} : \mathit{stack} \to X \to \mathit{stack}, \mathit{pop} : \mathit{stack} \to \mathit{stack}, \mathit{top} : \mathit{stack} \to X; construction \mathit{empty}, \mathit{push}\ \mathit{stack}\ X : \mathit{stack} (equivalently P\,\mathit{empty} \land (\forall s : \mathit{stack} \cdot \forall x : X \cdot P\,s \Rightarrow P(\mathit{push}\ s\ x)) \Leftarrow \forall s : \mathit{stack} \cdot P\,s); induction \mathit{empty}, \mathit{push}\ B\ X : B \Rightarrow \mathit{stack} : B (equivalently P\,\mathit{empty} \land (\forall s : \mathit{stack} \cdot \forall x : X \cdot P\,s \Rightarrow P(\mathit{push}\ s\ x)) \Rightarrow \forall s : \mathit{stack} \cdot P\,s), "to exclude anything else from being a stack"; "to say that the constructors always construct different stacks", \mathit{push}\ s\ x \neq \mathit{empty} and \mathit{push}\ s\ x = \mathit{push}\ t\ y = (s = t \land x = y); and "last in, first out": \mathit{pop}(\mathit{push}\ s\ x) = s, \mathit{top}(\mathit{push}\ s\ x) = x. A theory is a Lean structure DataStackTheory X — a carrier type (the bunch \mathit{stack}, taken as a type so that the operations are total on it), the four operations, and the axioms as fields; construction is automatic for a type, and both predicate forms are proved. Consequences: every stack is \mathit{empty} or a \mathit{push}, and the LIFO axioms alone make \mathit{push} injective. "According to the axioms we have so far" — before the last four — "it is possible that all stacks are equal": the one-element carrier satisfies the weak axioms, so \mathit{push}\ s\ x \neq \mathit{empty} is independent of them. Uses Definition 2.1, Definition 3.1 and Theorem 7.2.

"In the data-stack theory just presented, we have axioms \mathit{empty} : \mathit{stack} and \mathit{pop} : \mathit{stack} \to \mathit{stack}; from them we can prove \mathit{pop}\ \mathit{empty} : \mathit{stack}. ... An implementer is obliged to give a stack for \mathit{pop}\ \mathit{empty}, though it does not matter which one. If we never want to pop an empty stack, then the theory is too strong. ... For most purposes, it is sufficient to be able to push items onto a stack, pop items off, and look at the top item. ... Our simpler data-stack theory introduces the names \mathit{stack}, \mathit{push}, \mathit{pop}, and \mathit{top} with the following four axioms: \mathit{stack} \neq \mathit{null}, \mathit{push}\ s\ x : \mathit{stack}, \mathit{pop}(\mathit{push}\ s\ x) = s, \mathit{top}(\mathit{push}\ s\ x) = x." The design remarks are made concrete: every data-stack theory is a simple one, the list implementation is a model, and there is a model with no empty stack at all — infinite stacks \mathit{nat} \to X, in which every stack is a \mathit{push} ("we never need an empty stack, nor to test if a stack is empty"). "As an engineering activity, theory design is the art of excluding all unwanted implementations while allowing all the others." Uses Definition 8.1 and Theorem 8.2.

"The queue data structure, also known as a buffer ... is the structure with the motto: the first one in is the first one out. We introduce the syntax \mathit{queue}, \mathit{emptyq}, \mathit{join}, \mathit{leave}, and \mathit{front}." Axioms: \mathit{emptyq} : \mathit{queue}, \mathit{join}\ q\ x : \mathit{queue}; \mathit{join}\ q\ x \neq \mathit{emptyq}, \mathit{join}\ q\ x = \mathit{join}\ r\ y = (q = r \land x = y); queue induction \mathit{emptyq}, \mathit{join}\ B\ X : B \Rightarrow \mathit{queue} : B; and "first in, first out": \mathit{leave}(\mathit{join}\ \mathit{emptyq}\ x) = \mathit{emptyq}, q \neq \mathit{emptyq} \Rightarrow \mathit{leave}(\mathit{join}\ q\ x) = \mathit{join}(\mathit{leave}\ q)\ x, \mathit{front}(\mathit{join}\ \mathit{emptyq}\ x) = x, q \neq \mathit{emptyq} \Rightarrow \mathit{front}(\mathit{join}\ q\ x) = \mathit{front}\ q. The typing axioms q \neq \mathit{emptyq} \Rightarrow \mathit{leave}\ q : \mathit{queue} and q \neq \mathit{emptyq} \Rightarrow \mathit{front}\ q : X "can now be proved" (automatic for a carrier type). Derived: every queue is \mathit{emptyq} or a \mathit{join}, and the item joined to the empty queue stays at the front whatever is joined afterwards. "Data-queue implementation raises no new issues, so we leave it as Exercise 426": lists with \mathit{join}\ q\ x = q ;; [x], \mathit{leave}\ q = q\,[1;..\# q], \mathit{front}\ q = q\,0 are a DataQueueTheory ℤ. Uses Definition 8.1 and Theorem 4.10.

"We introduce the syntax \mathit{tree}, \mathit{emptree}, \mathit{graft}, \mathit{left}, \mathit{right}, \mathit{root}. For the purpose of studying trees, we want a strong theory": \mathit{emptree} : \mathit{tree}, \mathit{graft} : \mathit{tree} \to X \to \mathit{tree} \to \mathit{tree}, induction \mathit{emptree}, \mathit{graft}\ B\ X\ B : B \Rightarrow \mathit{tree} : B, \mathit{graft}\ t\ x\ u \neq \mathit{emptree}, \mathit{graft}\ t\ x\ u = \mathit{graft}\ v\ y\ w = (t = v \land x = y \land u = w), \mathit{left}(\mathit{graft}\ t\ x\ u) = t, \mathit{root}(\mathit{graft}\ t\ x\ u) = x, \mathit{right}(\mathit{graft}\ t\ x\ u) = u. "For most programming purposes, the following simpler, weaker theory is sufficient": \mathit{tree} \neq \mathit{null}, \mathit{graft}\ t\ x\ u : \mathit{tree} and the three selector axioms. Derived: every tree is \mathit{emptree} or a \mathit{graft}; the selectors alone make \mathit{graft} injective. The book's implementation by nested lists (\mathit{graft}\ t\ x\ u = [t; x; u], \mathit{left}\ t = t\,0, \mathit{root}\ t = t\,1, \mathit{right}\ t = t\,2) mixes lists and items and is not expressible with the homogeneous lists of Definition 4.9; the implementation here is the inductive type of finite binary trees — the recursive data definition \mathit{tree} = \mathit{emptree}, \mathit{graft}\ \mathit{tree}\ X\ \mathit{tree} as a datatype (cf. Definition 7.5) — with the book's example tree [[[\mathit{nil}]; 2; [[\mathit{nil}]; 5; [\mathit{nil}]]]; 3; [[\mathit{nil}]; 7; [\mathit{nil}]]]. Uses Definition 8.1.

"Users and implementers of a data structure can freely see and change their own variables, but they cannot freely see or change each other's variables. ... If we need only one stack ... we can obtain an economy of expression and of execution by leaving it implicit." "The simplest version of program-stack theory introduces three names: \mathit{push} (a procedure with parameter of type X), \mathit{pop} (a program), and \mathit{top} (of type X). ... The following two axioms are sufficient: \mathit{top}' = x \Leftarrow \mathit{push}\ x, \mathit{ok} \Leftarrow \mathit{push}\ x.\ \mathit{pop}." A program theory is a structure over a state type with \mathit{push} a parametrized specification, \mathit{pop} a specification and \mathit{top} a state variable, the axioms being refinements. "The second axiom says that a pop undoes a push. In fact, it says that any natural number of pushes are undone by the same number of pops: \mathit{ok} \Leftarrow \mathit{push}\ x.\ \mathit{pop} = \mathit{push}\ x.\ \mathit{ok}.\ \mathit{pop} \Leftarrow \mathit{push}\ x.\ \mathit{push}\ y.\ \mathit{pop}.\ \mathit{pop} ... We can prove things like \mathit{top}' = x \Leftarrow \mathit{push}\ x.\ \mathit{push}\ y.\ \mathit{push}\ z.\ \mathit{pop}.\ \mathit{pop}, which say that when we push something onto the stack, we find it there later at the appropriate time." Both are proved, the first for any number of push–pop pairs. Uses Definition 8.4, Definition 5.2 and Theorem 5.12.