一、规格化设计的发展历史
规格化设计的出现与发展和程序设计思想的发展密切相关，程序设计思想的发展大致如下：
1、1940年代：
最早被确认的现代化、电力引导的计算机约在1940年代被创造出来。程序员在有限的速度及存储器容量限制之下，撰写人工调整过的汇编语言程序。而且很快就发现到使用汇编语言的这种撰写方式需要花费大量的脑力而且很容易出错。
2、1950与1960年代
Fortran、LISP、COBOL三个现代编程语言于1950年代被设计出来，这三者所派生的语言直到今日仍旧广泛地被采用。由美国与欧洲计算机学者针对"算法的新语言"所组成的委员会出版的ALGOL 60报告也于1950年代晚期发布。
另一个创新则是关于语言的描述方式：一种名为巴科斯-诺尔范式 (BNF)的数学化精确符号被用于描述语言的语法。
3、1967-1978：
大多数现在所使用的主要语言范式都是在这段期间中发明的，如：Simula、C、Smalltalk、Prolog、ML。
4、1980年代：增强、模块、性能
在语言设计上有个重大的新趋势，就是研究运用模块或大型组织化的程序单元来进行大型系统的开发。Modula、Ada，以及ML都在1980年代发展出值得注意的模块化系统。
在模块化设计过程中，我们就要注重规格化设计。
规格化设计程序有许多优点，便于自己和别人理解程序，简化代码理解，可以加快开发速度，适合团队合作。规格化设计有助于提高代码的规范性，便于扩展和维护。按照规格化设计的程序，往往具有高可读性、统一的全局决策、清晰地逻辑处理、统一的规格规范、完善的逻辑判断、易维护性和高防御性。所以规格化设计得到了人们的重视。
二、规格bug
第九、十一次作业没有被报规格bug，这里仅列出第十次作业的bug。
| 序号 | 规格bug类别 | 错误原因 | 对应方法行数 |
| 1 | Effects逻辑错误 | Command类中addRespondTaxi方法EFFECTS使用自然语言描述 | 1 |
| 2 | Effects逻辑错误 | Taxi类中run方法使用自然语言描述 | 72 |
| 3 | Effects逻辑错误 | LightInfo类中readLight方法使用自然语言描述 | 38 |
三、规格bug产生的原因
1、没有按照先写规格，再写具体代码的方法。而是先写代码，再根据代码撰写规格，难免在规格书写过程中会有疏漏。
2、没有认真学习JSF的书写规范。由于对JSF规范没有全面掌握，因此在代码书写过程中会出现不符合规范的写法。
3、大量使用自然语言，部分方法没有用布尔表达式来书写规格。
4、由于程序设计前考虑不周，导致部分方法写得过于冗杂，部分方法有好几十行，这给规格的书写带来了极大的不便，容易出现逻辑错误及不完整的情况。
四、不好的写法及改进
前置条件
No.1 未对函数传入的参数进行限制。改进方法：对传入的参数进行限制。
public void addRespondTaxi(Taxi taxi) @REQUIRES: none//改进后@REQUIRES: taxi != null
No.2 各布尔表达式之间用，连接。改进方法：各布尔表达式之间用&&连接。
public Command(int srcX,int srcY,int dstX,int dstY,double time,long longtime,String str)@REQUIRES: 0<=srcX<80,0<=srcY<80,0<=dstX<80,0<=dstY<80//改进后@REQUIRES: 0<=srcX<80 && 0<=srcY<80 && 0<=dstX<80 && 0<=dstY<80
No.3 前置条件使用自然语言。改进方法：按照JSF规范书写。
public void addCommand(Command command)@REQUIRES:command非空且合法//改进后@REQUIRES: command!=null
No.4
public LightThread(int[][]lightExist,int[][] light,TaxiGUI gui)@REQUIRES: 各参数合法//改进后@REQUIRES: lightExist!=null && light!=null && gui!=null
No.5
public void setLightExist(int[][] newLightExist) @REQUIRES: none//改进后@REQUIRES: newLightExist != null
后置条件
No.1 对于用synchronized修饰的方法，未给出THREAD_REQUIRES和THREAD_EFFECTS。改进方法：加入THREAD_REQUIRES和THREAD_EFFECTS。
public synchronized void setCredit(int newCredit) { /** * @REQUIRES: newCredit>0 * @MODIFIES: this * @EFFECTS: this.credit==newCredit */ this.credit=newCredit; } //改进后 /** * @REQUIRES: newCredit>0 * @MODIFIES: this * @EFFECTS: this.credit==newCredit * @THREAD_REQUIRES: \locked(\this); * @THREAD_EFFECTS: \locked(); */ No.2 EFFECTS使用自然语言。改进方法：使用布尔表达式书写。
public void addRespondTaxi(Taxi taxi) { /** * @REQUIRES: taxi != null * @MODIFIES: this * @EFFECTS: Add a new taxi to the respondTaxi */ respondTaxi.add(taxi); } //改进后 /** * @REQUIRES: taxi != null * @MODIFIES: this * @EFFECTS: respondTaxi.contains(taxi) */ respondTaxi.add(taxi); } No.3 EFFECTS中的布尔表达式中，使用=。改进方法：将=改为==。
public synchronized void setTowards(int num) { /** * @REQUIRES: 0<=num<=4 * @MODIFIES: this * @EFFECTS: this.towards = num */ this.towards=num; } //改进后 /** * @REQUIRES: 0<=num<=4 * @MODIFIES: this * @EFFECTS: this.towards == num */ No.4 减少自然语言的使用
public void clearFlux() { /** * @REQUIRES: none * @MODIFIES: this * @EFFECTS: set flux to 0 */ for(int i=0;i No.5
public void addFlux(int a,int b) { /** * @REQUIRES: 0<=a<6400 && 0<=b<6400 * @MODIFIES: this * @EFFECTS: increase flux[a][b] and flux[b][a] and update GUI. */ if(guigv.m.graph[a][b]==1) { flux[a][b]++; flux[b][a]++; int aX=a/80; int aY=a%80; int bX=b/80; int bY=b%80; guigv.AddFlow(aX,aY,bX,bY); } } //改进后 /** * @REQUIRES: 0<=a<6400 && 0<=b<6400 * @MODIFIES: this * @EFFECTS: (guigv.m.graph[a][b]==1) ==> (flux[a][b]==\old(flux[a][b])+1 && flux[b][a] == \old(flux[b][a])+1). */ 五、功能bug与规格bug的聚集关系
三次作业中出现的功能bug
| 作业次数 | 功能bug | 引起bug的方法 |
| 第九次 | Taxi类中随机移动函数有误，导致出租车线程在LoadFile后可能会crash | Taxi类move函数 |
| 第十次 | 出租车随机移动出现回头现象 | FluxThread类中的流量相关方法和Taxi类move函数 |
| 第十次 | 输入多条指令，程序可能输出“地图不联通，程序退出” | gui.java中的求最短距离的方法线程不安全 |
| 第十一次 | 程序最小时间单位不是100ms | 直接将系统时间作为时间（100ms其实只是用来判断同质请求的） |
三次作业的功能bug和规格bug
| 作业次数 | 功能bug个数 | 规格bug个数 |
| 第九次 | 1 | 0 |
| 第十次 | 2 | 3 |
| 第十一次 | 1 | 0 |
产生功能bug的方法和产生规格bug的方法并不相同，所以功能bug和功能bug并没有直接的聚集关系。
六、个人心得
1、规格的设计和撰写很重要，在写代码时，应当先分析要求，考虑到各个方面，先写规格，再实现具体代码，这样写出来的代码符合最初设计的要求，也不容易出现bug。
2、按照JSF的规范来书写，尽量减少自然语言的使用。使用JSF规范书写代码，有助于提高我们书写规格的逻辑性与规范性，这对我们的学习及未来走上工作岗位都是很有用的。