抽象数据类型

ADT 的动机是把“对象能做什么”与“对象如何存”分开：接口回答前者，实现回答后者。这一分离让使用者只依赖可观察行为，于是实现可以整体替换而无需改动调用方；正确性论证也可以分层——先证实现满足规格，再证客户端只使用规格允许的事实。可以把 ADT 理解成一份合同：操作签名规定可以提出哪些请求，代数公理或状态转移规定请求的结果，表示则留给实现选择。ADT 因而不是某个具体数据结构；同一抽象值常对应多个具体状态，抽象函数 $\alpha$ 正是把这种多对一关系压平。

栈是标准正例：栈公理库栈Stack · LIFO stack只在同一端插入和删除、遵循后进先出的结构。的签名含 push、pop、top 与判空，公理包括 $\mathrm{top}(\mathrm{push}(s,x))=x$、$\mathrm{pop}(\mathrm{push}(s,x))=s$ 以及新建栈为空。仅由公理即可推出后进先出行为：连续压入 $x,y$ 后，第一次 top 得到的是 $y$ 而非 $x$。用定长数组公理库数组Array以连续整数下标支持随机访问的有限序列结构。加栈顶下标实现时，表示不变式是“栈顶下标不超过容量”，抽象函数把前若干个槽位读成栈内容；用链表公理库链表Linked list节点通过指针连接并支持局部插入删除的线性数据结构。实现时对应另一组 $\mathrm{Inv}$ 与 $\alpha$——两种实现的外部行为不可区分。

边界之一：签名相同不代表 ADT 相同。队列公理库队列Queue · FIFO queue在尾部插入、头部删除、遵循先进先出的结构。与栈的操作名几乎可以一一对应，但公理不同（先进先出对后进先出），因此是不同的类型；决定 ADT 的是语义规律而非函数名。边界之二：复杂度默认不属于规格。数组栈与链表栈都正确，但扩容等成本行为不同；只有把成本写进接口契约（如“摊还常数时间追加”），它才成为规格的一部分。此外，实现若泄露内部表示（例如把内部结点的引用交给调用方），表示不变式就可能被外部代码破坏，抽象随之失效。

表示独立性要求客户端无法凭合法接口区分两个正确实现，而不是要求它们的内部状态逐字相同。例如集合接口只暴露插入、删除和成员判断时，客户端不应观察元素落在哪个哈希桶或树结点；一旦内部位置成为可观察结果，原规格就必须扩展，原有的互换性也不再成立。形式证明常用表示关系把两个实现的具体状态配对，并证明每次对应操作后这一关系仍保持。

ADT 是模块化验证与表示独立性的基础。客户端算法的功能正确性只依赖接口公理；选定具体表示后，复杂度分析才把各操作的最坏、摊还或期望代价代入。若接口确实要求某种成本，例如“追加操作具有摊还常数时间”，就应把它明确写成带成本的规格，而不能把某个实现的性能表默认为抽象类型的语义。具体的栈、队列、映射或优先队列只是这一分层的实例，不构成 ADT 定义本身。