一、规格化设计的历史以及人们重视的原因
发展历史
从20世纪60年代开始，就存在着许多不同的形式规格说明语言和软件开发方法。在形式规格说明领域一些最主要的发展过程列举如下：
1969－1972 C.A.R Hoare撰写了"计算机编程的公理基础（An Axiomatic Basis for Computer Programming）"和"数据表示的正确性证明"两篇开创性的论文，并提出了规格说明的概念。
1974－1975 B.Liskow/S.N. Zilles和J. Guttag引入了"抽象数据类型"的概念。
1976 E.W. Dijkstra定义了"最弱前置条件"的概念
1977 R.Burstall和J.Goguen提出了第一个代数规格说明语言：Clear
1988 Standford的SRI开发了代数规格说明语言OBJ3
1980-1986 C.Jones定义了VDM语言，也就是维也纳开发方法。
1985－1992 牛津大学的程序研究小组开发了Z规格说明语言。与此同时BP研究室开发了称之为B方法的面向模型的规格说明语言。
1985－1993 在MIT和Digital SRC开发了代数规格说明语言Larch
从1991年开始，面向对象的形式规格说明语言开始发展，例如，Object-Z, VDM++, CafeOBJ等语言。
1996－2000年 在欧洲CoFI（Common Framework Initiative）项目资助下开发"统一"代数规格说明语言CASL(Common Algebraic Specification Language)
重视原因
我认为规格首先给了大家编程时一个统一的认识，明确了程序运行的前提和程序运行后的效果，这一点在个人编程中有助于理清思路，而在集体的工程开发过程中也有助于协作，使大家开发的方向一致。
另一方面我认为正确的规格可以方便编程者进行调试，通过断言判断前置条件是否满足以及检验后置条件是否在程序运行后满足。
二、规格Bug数量及原因分析
| 作业 | Bug类型及细节 | 所在文件及行数 |
| 第九次 | 无 | 无 |
| 第十次 | Effects内容为实现算法： esult写成了 eturn | 很多文件中 |
| 第十一次 | Effects不完整：在有try-catch的方法中忘记写exceptional_behavior | InputHandler.java/192 |
规格bug原因分析：第九次没有被报规格bug，大概是测试者不太关心。第十次和第十一次作业中都是有所疏忽导致。其中第十次作业是一个笔误，几乎所有文件都写成了 eturn==balabala，第十一次作业中有一个方法由于后来有改动，没有添加exceptional_behavior。
三、不好的规格写法及改进
前置条件
1. 自然语言描述
1 /** 2 * @REQUIRES: k存在 3 * @MODIFIES: v 4 * @EFFECTS: v == old(v) + 1; 5 */
1 /** 2 * @REQUIRES: k != null 3 * @MODIFIES: v 4 * @EFFECTS: v == old(v) + 1; 5 */
2. 不是布尔表达式
/** * * @REQUIRES: * this.taxiStatus = IDLE; * @MODIFIES: * this.credit; * @EFFECTS: * this.credit = old(this.credit) + 1; * (all PassengerRequest r in range, r.grabbedByTaxi(this)) * */
/** * * @REQUIRES: * this.taxiStatus == IDLE; * @MODIFIES: * this.credit; * @EFFECTS: * this.credit = old(this.credit) + 1; * (all PassengerRequest r in range, r.grabbedByTaxi(this)) * */
3. 没有规定范围
/** * * @REQUIRES: * locX, locY, dstX, dstY； * @MODIFIES: * edge between (locX, locY),(dstX, dstY), ConsolePrinter; * @EFFECTS: * edge.existence == op; * */
/** * * @REQUIRES: * 0 <= locX, locY, dstX, dstY <= 79; * @MODIFIES: * edge between (locX, locY),(dstX, dstY), ConsolePrinter; * @EFFECTS: * edge.existence == op; * */
4. 遗漏了某些条件，一般是传入参数外的某些条件
/** * @REQUIRES: mapVertex != null; * @MODIFIES: ConsolePrinter * @EFFECTS: esult == the opposite vertex of mapVertex */
/** * @REQUIRES: mapVertex != null && mapVertex.repOK == true; * @MODIFIES: ConsolePrinter * @EFFECTS: esult == the opposite vertex of mapVertex */
5. 对于一个容器中的所有对象，均需要规定前置条件
/** * * @REQUIRES: * this.edgeMap != null * @MODIFIES: * None * @EFFECTS: * (exist MapEdge e, edgeMap.contains(e), min(edgeMap.flowrates) == e.flowrate && esult == e); * * @THREAD_EFFECTS: * ( all MapEdge e in this.edgeMap); */
/** * * @REQUIRES: * ( all MapEdge e, this.edgeMap.contains ( e), e != null) * @MODIFIES: * None * @EFFECTS: * (exist MapEdge e, edgeMap.contains(e), min(edgeMap.flowrates) == e.flowrate && esult == e); * * @THREAD_EFFECTS: * ( all MapEdge e in this.edgeMap); */
后置条件
1. 不是布尔表达式
/** * * @REQUIRES: * this.requestQueue != null * @MODIFIES: * None * @EFFECTS: * return this.requestQueue; * */
/** * * @REQUIRES: * this.requestQueue != null * @MODIFIES: * None * @EFFECTS: * esult == this.requestQueue; * */
2. 返回容器时不够明确
/** * * @REQUIRES: * this != null * @MODIFIES: * None * @EFFECTS: * esult == (all MapEdge e in this.edgeMap) * */
/** * * @REQUIRES: * this != null * @MODIFIES: * None * @EFFECTS: * esult == new Arraylist<MapEdge> r; * (all MapEdge e, this.edgeMap.contains(e), r.contains(e)) * */
3. 改变值书写不规范
/** * * @REQUIRES: * this != null, num > 0; * @MODIFIES: * this.credit; * @EFFECTS: * this.credit += num; * */
/** * * @REQUIRES: * this != null, num > 0; * @MODIFIES: * this.credit; * @EFFECTS: * this.credit == old(this.credit) + num; * */
4. 没有写异常情况
/** * @REQUIRES: * this.list != null; * @MODIFIES: * None * @EFFECTS: * this.hasNext() ==> ( esult == this.list[old(index)+1] && index == old(index) + 1); * * @THREAD_EFFECTS: * locked(this.list); */
/** * @REQUIRES: * this.list != null; * @MODIFIES: * None * @EFFECTS: * this.hasNext() ==> ( esult == this.list[old(index)+1] && index == old(index) + 1); * exceptional_behavior(NoSuchElementException) * * @THREAD_EFFECTS: * locked(this.list); */
5. 后置条件没写全
/** * @REQUIRES: key != null; * passengerRequest != null; * @MODIFIES: this.unprocessedRequests, ConsolePrinter; * @EFFECTS: unprocessedRequests.contains(passengerRequest); * @THREAD_EFFECTS: locked(this.appendlock); */
/** * @REQUIRES: key != null; * passengerRequest != null; * @MODIFIES: this.unprocessedRequests, ConsolePrinter; * @EFFECTS: unprocessedRequests.contains(passengerRequest); unprocessedRequests.size == old(unprocessedRequest).size + 1 * @THREAD_EFFECTS: locked(this.appendlock); */
四、功能Bug与规格Bug的聚类关系
本人仅在第九次作业中被报了功能bug，分别是输入格式错误会导致crash（说好的测试者保证呢）以及bfs在添加流量后判断条件有误导致找出了流量最小而不是距离最近的道路（在车聚集在一堆的时候可能绕路）。
之后的jsf问题我认为均是格式或者规范问题，与功能并没有什么关系，基本上都是功能实现正确但jsf写的时候可能有所遗漏。
五、撰写规格的思路与体会
之前写作业往往是先写程序代码最后再写规格，后来有尝试先写规格再改程序代码。规格的问题往往出在改正了程序的代码，然后程序跑着没什么问题了，结果改的地方一多就忘记改规格了。虽然看群里大家对于JSF的设计都有些抱怨，但JSF在复查代码的方面的确有一定的帮助，也对我形成工程化思想有了一些小小的推动作用。
希望课程组可以逐渐完善JSF，起码现在感觉很多复杂的逻辑用JSF表达起来非常费力以至于不得不用自然语言。