前言 本文将介绍一些关于ADT设计中Spec、AF和RI细节。由于内容细碎，为了加强理解，列出了这部分知识点，进行了简单的总结。

一. Spec

当我第一次接触软件结构时，关于规定Spec这个概念已经被接触到了，但是在实验中设计规则的时候才真正开始理解。

（一）含义

Spec是程序员设计的ADT规定你写的方法时，它规定了方法应该做什么，不应该做什么。在下一个设计中，测试用例的编写需要依靠Spec因为程序员编写的代码必须符合spec是的，否则就不合格。同时，有了Spec客户端在使用代码时会有一些基础，好的Spec可以大大节省客户端使用自己的用途API所需的时间大大降低了客户端对自己编写代码的误解。

(二)内容及评价标准

Spec主要内容分为以下三部分：

1. 前置条件precondition：这是对客户端的约束，是用户在使用方法时必须满足的条件。Java一般使用声明@param说明每个参数的前提。

2. 后置条件postcondition：这是对开发者的约束，也是设计师在方法结束时必须满足的。Java一般使用以下两种声明，其内容和用途如下：

@return：对后置条件的说明一般为返回值； @throws：说明异常时会发生什么，一般是异常处理。

（三）Spec强弱

若想要Spec变强，可以采用如下方式：

1. 前置条件更宽松

2. 后置条件更严格

如果在图中使用椭圆对不同的椭圆，Spec强弱进行表示，则越小（包含的结果的点越少）的椭圆，其Spec我们可以理解，椭圆的大小代表了开发者的自由。

(四)注意事项

程序员应该通过Spec让客户轻松知道他需要为这种方法提供什么参数和结果，但用户不应该知道该方法的内部逻辑，以避免恶意用户对代码结构的损害。

二. AF和RI

由于AF和RI两者之间有映射关系，可以一起讨论。

（一）含义

RI：Rep Invariant。其中Invariant是不变量的意思，是的ADT在任何时候都应该满足的一些条件。

AF：Abstraction Function。代表抽象函数。

(二)具体表示

AF和RI中的A和R分别代表两个空间：R是开发者关注的内部空间；A是ADT客户存在的对象一般都是客户关注的。

而AF就是从R空间到A空间的一个映射，作为解释函数，对A空间的每一个对象，在R空间中都至少由一种属性或类型与之对应，因此该映射是一个满射。

而RI是R空间中所有值的子集，包含所有法定表示值。checkRep()方法是随时检查RI是否满足。

附上自己在这里lab2中写过的AF、RI，以及Safety from rep exposure的描述：

// Abstraction function // AF(vertices) = 点集 // Representation invariant: // 无重复点 // Safety from rep exposure: // private final List<Vertex<L>> vertices

（三）注意事项

RI、AF关系如下：

同一R可能有不同的RRI；

即使是一样的R、 RI，也可以根据不同的解释获得不同的解释AF；

两个ADT有相同的rep和相同的AF，但是R也不一样。

不应该给client看的内容有AF、RI、Rep exposure safety argument、testing strategy、Rep、Implementation和Test cases等等，留给client的只有Spec。

总结

本文主要解释了一些ADT设计中关于Spec、AF和RI含义、内容、注意事项等。细节比较琐碎，但在实际应用中非常重要，所以以以后有需要的时候要记住和学习。