一、规格化设计的发展历史
最早的程序设计是采用机器语言编写的，然而，由于机器语言的编写难度过高，于是便发展出了编程语言以及后来的面向过程语言。然而，在1968年，Dijkstra提出了GOTO语句有害论，包括不易测试、限制代码优化等缺点，从而引发了软件界长达数年的论战，并由此产生了结构化程序设计的思想。而Pascal语言也作为第一个结构化的语言就此问世。
结构化设计的本质仍然是面向过程的设计思想，但是通过模块化、自顶向下等方法，使得软件的复杂度保持在一定范围之内，从而降低了整个软件开发的复杂度。然而，随着现代社会的发展，结构化设计已经逐渐无法满足硬件和业务的发展，使得第二次软件危机到来。在第二次软件危机的背景下，面向对象的设计思想得以高速发展。
软件的开发常常都不是由一个人独立完成的，需要多人协同完成。那么，在这个协作的过程中，不同的开发者之间或者开发者与设计者之间，如果仅仅需要关心某个函数的接口的需求以及会修改的数据，那么无疑能使工作更有效率，也有利于后期对于软件的维护与修改。
二、规格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阐述出来，仅能通过自然语言表述。
第十一次作业
无
三、规格bug产生原因
规格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：后置条件一般是将方法的作用结果通过布尔表达式的形式给出，但有时由于设计的部分方法较为复杂或者其他原因导致不能很好的利用布尔表达式表达出来，不得不使用自然语言表述。这种情况下，可以考虑简化、拆分方法的功能，或是问问其他同学对于功能复杂方法的后置条件如何进行表述。
原文：https://www.cnblogs.com/98-0901/p/9106506.html