抽象数据类型

使用栈时，客户端关心最后压入的元素最先弹出，而不关心元素放在连续内存里，还是由链表节点连接。栈规范确定后进先出的行为；数组和链表是在兑现这份规范的不同实现。

这种分离让内部结构可以改变，却不迫使所有调用者跟着改。前提是客户端只依赖公开契约：若它越过接口读取内部数组、假定某次遍历恰好采用当前哈希顺序，就已经把实现细节当作承诺。随后更换合法实现时，原本未被保证的行为没有义务继续保持。

抽象函数把许多具体状态看成同一个值；表示不变量则先排除根本不应解释的状态。两者不能混淆：容量不同的两个数组可以是同一个合法栈，而长度超过容量的数组记录是非法表示，不能靠给它勉强指定一个抽象值来补救。这一区别决定了实现证明先检查哪些条件，再比较哪些可观察结果。

类和 ADT 因而不是同义词。一个类可以实现 ADT，也可以只是暴露一堆字段；同一个 ADT 可以用类、模块或其他封装机制实现。真正建立抽象边界的是可观察行为的规范与表示隐藏，而不是是否使用了某个关键字。

一份完整的栈契约 ​

令抽象栈状态为有限序列 $s=[a_1,\dots ,a_k]$，按栈底到栈顶排列。初始状态为 $[]$。操作约定为：push(x) 将状态变成 $s++[x]$；isEmpty 返回 $k=0$ 的真假；对非空栈，top 返回 $a_k$ 且不改变状态，pop 返回 $a_k$ 并将状态变成 $[a_1,\dots ,a_{k-1}]$。

这里把返回值与状态变化明确分开了。若从空栈调用 top 或 pop，本例规定返回带标签的 EmptyStack 错误并保持空状态。另一份规范也可以将非空设为前置条件，但那是不同的契约选择，不应在同一条推理中来回切换。

由此，任意栈 $s$ 上先 push(x) 再 pop，都会返回 $x$ 并恢复 $s$；先 push(x) 再 top 则只观察 $x$，不会撤销压栈。这些可执行的行为规律比只列出方法名称更能定义一个栈。

两种表示怎样对应同一个抽象状态 ​

动态数组实现可保存数组 $a$、有效长度 $k$ 与容量 $c$，不变量包括 $0\le k\le c$，抽象函数读出前 $k$ 个有效元素：$\alpha (a,k,c)=[a[0],\dots ,a[k-1]]$。同一抽象栈可以有不同容量，所以抽象函数通常不是单射。扩容复制只要保留这段序列，就没有改变抽象值。

例如底层为 $[a,b,\mathrm{\_},\mathrm{\_}]$、$k=2,c=4$ 时，抽象状态是 $[a,b]$。执行 push(x) 先把新值写入槽 $2$，再令 $k=3$，得到抽象状态 $[a,b,x]$；原来的两项保持不变，且 $3\le 4$，于是状态转移和表示不变量都满足。若实现只改槽位却忘记增加 $k$，底层看似已经写入，抽象栈却没有变化，恰好违反 push 的契约。

链表实现可以把栈顶放在表头。例如表头到表尾为 $c\to b\to a$，抽象栈便是 $[a,b,c]$。不变量需保证链表有限、无环、指针合法；从表头插入或删除节点恰好对应抽象栈顶的变化。

本例抽象栈没有固定的最大长度。容量永远固定为 $c$ 的数组不能无条件实现它：第 $c+1$ 次连续压栈会遇到规范中没有规定的限制。要么使用能扩容的表示并另行说明资源失败行为，要么定义一个带容量与溢出行为的有界栈 ADT。

满足同一规范不必逐次输出相同 ​

若集合 ADT 只保证迭代返回每个元素一次、不保证顺序，一个实现返回 a,b，另一个返回 b,a，都可能符合契约。它们对“取第一个元素”的观察不同，却不能因此判定其中一个错误。

因此，证明实现符合一个允许多种行为的规范，通常得到的是行为精化：实现选择的行为属于规范允许的范围。只有在更明确的条件下，例如确定且充分规定的可观察语义，以及合适的封装假设，才能继续证明两个实现对客户端观察等价。规范符合性与观察等价不能直接画等号。

表示不变量支撑模块化证明 ​

证明一个数据结构正确，可以按初始化和每个操作分别进行。初始化建立不变量；每个操作在合法表示与前置条件下保持不变量，并经 $\alpha$ 对应到规定的抽象变化。客户端随后只需使用抽象契约推理，不必再次展开数组移动或链表指针更新的细节。

这也要求防止表示泄漏。若接口把内部可变数组直接交给客户端，客户端就可能绕过操作修改元素、破坏不变量；只在公开方法入口检查一次并不能恢复真正的封装。返回不可变视图、受控副本或明确的共享协议，是不同的边界设计。

计数器的表示独立性证明理路表示独立性Representation independence · Representation independence theorem以自然数和单位列表计数器为例，逐项证明接口关系，再对纯传值客户端的全部构造归纳，覆盖高阶调用与抽象状态递归。进一步固定存在接口和纯传值客户端语言，以自然数与单位列表为两种表示。它从接口保持关系证明所有允许客户端观察相同，包含保留旧状态、高阶调用和分支；这个量词结论需要语言封装及客户端归纳，不能只从两种实现各自符合宽泛规范推出。

行为、成本与并发要求分别写清 ​

动态数组栈的压栈可以具有摊还 $O(1)$ 成本，却在扩容的某一次调用花费 $O(n)$；链表实现可以用不同的分配和局部性代价兑现相同的顺序行为。若接口承诺最坏单次延迟，不能拿摊还界来替代；若契约未限制时间，功能等价也不会自动推出性能相近。

并发实现还需要说明多个重叠操作如何对应抽象行为。线性化要求：对每个有限调用历史，可补全部分未完成调用、删除其余未完成调用，使得到的完成历史对应某个合法顺序历史，并尊重调用线程内顺序与已完成操作的实时先后。仅证明每个方法单独看都“像栈操作”，不足以保证组合执行仍表现为同一个栈。

ADT 因而提供一条分层路线：先写出可观察行为，再选择表示并证明其正确，最后在需要时增加成本与并发保证。每一层的结论都有明确的契约依据，而不是由数据结构名字自动带来。