一、规格化设计的发展历史及得到重视的原因
（1）发展历史
确保程序的正确性以及减少软件的错误一直是人们所关心的问题，然而随着软件系统越来越复杂，在规模与功能上都有大幅度的扩展，更需要一种规范的设计方法来提高工作的效率与正确性。
1959年，Hoare提出了基于“前置后置条件”的接口规格方法，该种思想指出只要一个方法能在其执行前满足前置条件并且执行后满足后置条件，那么便能确保该方法的正确性。Hoare的这个思想的提出为类中接口的规格化提供了理论基础。
在第二次软件危机中发展起来的面向对象语言，用旧的Hoare的理论已经难以适应，需要对其进行发展、扩展。Goguen和Zilles强调代数化方法，使用代数化方法验证抽象数据类型的规格化的正确性。然而，抽象数据类型虽然能够描述方法直接的关系，但却失去了对于单个方法的准确规格定义。
而为了实现单个方法的精确规格定义，Meyer提出了契约式编程，但是其是依赖于内部状态来体现方法之间的相互依赖。Robert也引入契约的思想来表达前置与后置条件。然而，契约式均以可编译的方式将前置、后置条件嵌入程序之中，使得其与程序语句之间很难区分开，影响了代码的阅读以及执行效率。
Yoonsik尝试使用模型方法与模型变量来解决以上问题，并建立了规格方法JML。其使用抽象的模型变量来代表内部数据状态，模型方法使用模型变量进行规格，这种方法虽然避免了程序代码与规格的混淆，却忽视了模型变量定义的难度，而这将导致运行时难以断言检查。
其他研究者也提出了使用状态抽象的方法进行类的规格定义。
[1]王伟,丁二玉,骆斌.基于抽象状态的类的行为规格化方法[J].计算机科学,2016,43(S1):457-460.
（2）受到重视的原因
软件的开发常常都不是由一个人独立完成的，需要多人协同完成。那么，在这个协作的过程中，不同的开发者之间或者开发者与设计者之间，如果仅仅需要关心某个函数的接口的需求以及会修改的数据，那么无疑能使工作更有效率，也有利于后期对于软件的维护与修改。
二、规格bug
第九次作业
| 编号 | 类别 | 所在方法 | 方法代码行数 |
| 1 | 不符合JSF规范 | Map类的shortestPath方法 | 43 |
Map类中的shortestPath方法为求最短路径的算法实现，但在EFFECTS中采用了自然语言描述，而未采用布尔表达式形式。
第十次作业
| 编号 | 类别 | 所在方法 | 方法代码行数 |
| 1 | Overview是否明确抽象对象 | Light类 | 101 |
| 2 | 不符合JSF规范 | Light类的refresh方法 | 4 |
| 3 | 不符合JSF规范 | Car类的dir方法 | 9 |
由于对于抽象对象的理解不是很深，故未能在Overview中明确抽象对象。另外，对于一些代码行数较短且中间涉及到一些返回计算出的中间变量的值的方法，不能很好的用布尔表达式的形式将其EFFECTS阐述出来，仅能通过自然语言表述。
第十一次作业
无
三、规格bu*生原因
规格bug出现的主要原因在于部分类的方法的具体功能不是很明确，并且以往缺乏对于规格撰写的经验，因此在撰写EFFECTS很难用布尔表达式表达出来，往往只能采用自然语言进行阐述，这就造成了JSF格式上的不规范。
四、前置、后置条件及其改进
前置条件
| 编号 |
方法 | 原写法 | 改进 |
| 1 | CarInfo类的output | None | path1!=null && path2!=null |
| 2 | Light类的initlight | filename!=null | filename!=null && status!=null && status.size>=6400 |
| 3 | Map类的create | None | filename!=null |
| 4 | Map类的initroad | None | map!=null && road!=null && road.size>=6400 |
| 5 | Passenger类的getserve | None | avaiable!=null |
后置条件
| 编号 |
方法 | 原写法 | 改进 |
| 1 | Car类构造方法 | initialize the elements in this class | (\result==this) && (this.id==id) && (this.type==type) && (this.credit==0) && (this.status==0) && (this.dir=='M') && (this.position!=null && 0<=this.position.x<80 && 0<=this.position.y<80) |
| 2 | Map类的shortestPath | path contains the Point from src to dst | (\all int i,j;i>=0,j=i+1,j<\result.length)==>(this.isConnect(\result[i],\result[j])==true) |
| 3 | Passenger类的peek方法 | (\exist Passenger p;p is the first element of queue) ==> \result == p; | \result==this.queue.peek() |
| 4 | CarInfo类的output | None | (path1.isEmpty==true) && (path2.isEmpty==true) |
| 5 | Light类的initlight | (\all int i;0<=i<6400)==>(0<=status[i]<=2) | ((\all int i;0<=i<6400)==>(0<=status[i]<=2)) && (this.time>0) |
五、功能bug及规格bug聚集关系
第九次作业
| 编号 | 方法 | 功能bug | 规格bug |
| 1 | Map类的shortesPath | 0 | 1 |
第十次作业
| 编号 | 方法 | 功能bug |
规格bug |
| 1 | Light类的refresh |
0 |
1 |
| 2 | Car类的dir | 0 | 1 |
| 3 | Passenger类的run | 1 | 0 |
第十一次作业
| 编号 | 方法 | 功能bug | 规格bug |
| 1 | Car类的run | 1 | 0 |
六、设计规格和撰写规格的基本思路与体会
（1）设计规格
在设计规格时，应当对于该方法的输入输出的数据进行数据结构的选择，并确定在方法执行后输出的数据不会出现偏差，即输入的数据必能得到一个合理的返回结果。另外，规格应当能屏蔽掉方法内部的具体算法流程，只保留面向使用者的输入输出接口信息以及相应的条件。
（2）撰写规格
（1）REQUIRES：前置条件一般是从传入的参数下手，若是一般的int类型数据，可要求其在该项数据使用的合法范围内；其它自定义的数据类型等可要求其不为null或是其他的约束条件；另外，若是方法中调用了该类中的某项属性，若该属性存在某种约束条件，应当一并列出。
（2）MODIFIES：这部分主要是向使用者描述方法对哪些属性进行了修改。
（3）EFFECTS：后置条件一般是将方法的作用结果通过布尔表达式的形式给出，但有时由于设计的部分方法较为复杂或者其他原因导致不能很好的利用布尔表达式表达出来，不得不使用自然语言表述。这种情况下，可以考虑简化、拆分方法的功能，或是问问其他同学对于功能复杂方法的后置条件如何进行表述。