一、规格化设计发展历史和优势
在1940年以前，人们采用直接编写二进制的方式产生机器能够识别的指令和数据。这种原始的编程方式操作难度大、出错率高，于是诞生了面向过程式的高级编程语言。由此编程开始脱离机器，而更多关注软件本身。
60年代之后，人类经历了两次软件危机。第一次危机之后，结构化的程序设计逐渐取代了goto语句导致的面条式代码。但随着软件需求越来越复杂和编程领域的扩大，第二次危机爆发后，面向对象成为了主流的开发思想。这种思想更接近人的自然思维，强调代码的工程化、模块化。在这一基础上，规格化的设计开始形成和发展，从输入输出中提取数据信息加以约束，在方法的构造者和调用者之间形成契约，淡化对算法本身实现细节的关注。这样一来，大大提高了整个工程项目的可扩展性和可维护性。
二、历史规格bug分析
|
作业 |
类名/方法名 |
bug类型 |
代码行数 |
|
第九次 |
Taxi/run |
EFFECTS不完整 |
36 |
|
第十次 |
fileHandler/readFile |
对于一个方法，方法做的修改不会修改repOK |
37 |
|
第十一次 |
无 |
无 |
无 |
三、规格bug产生原因分析
第一次的EFFECTS不完整是因为Taxi的run方法忘记写后置条件了。但也不完全是粗心的原因，是因为run方法对对象做的修改比较复杂，所以一时没有想好该怎么表述。但是现在看来其实可以采用自然语言尽量描述清楚，在后两次作业中改掉了这一问题。
第二次被报repOK是与读文件相关。我在rep里面规定了文件存在可读，但是当时写这个类的时候有点脑抽写了一堆静态方法没有写构造……所以在文件读入之前，就不能保证rep为真，之后删去了静态属性，加上了构造方法。
四、写法改进
1、前置条件：
(1)、public Taxi(int id, ArrayList[] map) {
/**
* @REQUIRES: (\all int i; 0<=i<Main.SIZP; map[i]!=null)
改为：
public Taxi(int id, ArrayList[] map) {
/**
* @REQUIRES: 0<=id<Main.TNUM && map!= null && (\all int i; 0<=i<Main.SIZP; map[i]!=null)
(2)、private void shortPath(int start, int end) {
/**
* @REQUIRES: None
改为：
private void shortPath(int start, int end) {
/**
* @REQUIRES: 0<=start<Main.SIZP && 0<=end<Main.SIZP && start is connected to end
(3)、* @REQUIRES: this.reqNow != null && 0<=this.reqNow.getDst()<Main.SIZP
改为：
* @REQUIRES: this.reqNow != null && 0<=this.reqNow.end<Main.SIZP
(4)、public Road(ArrayList<Integer>[] points, File testFile, int s, int n) {
/**
* @REQUIRES: testFile.exists && (\all int i; 0<=i<Main.SIZP; points[i]!=null)
改为：
public Road(ArrayList<Integer>[] points, File testFile, int s, int n) {
/**
* @REQUIRES: testFile.exists && points!=null && (\all int i; 0<=i<n; points[i]!=null) && n==s*s
(5)、* @REQUIRES: 0<=p1<this.num && 0<=p2<this.num && edges[p1].contains(p2) && edges[p2].contains(p1)
改为：
* @REQUIRES: 0<=p1<this.num && 0<=p2<this.num && (\exist Edge e; e is from p1 to p2)
2、后置条件：
(1)、@EFFECTS: this.flow != null && this.lastFlow != null;
改为：
@EFFECTS: this.flow == new int[n][4] && this.lastFlow == new int[n][4];
(2)、@EFFECTS: this.lastFlow == this.flow && this.flow == new int[this.num][4];
改为：
@EFFECTS: this.lastFlow == (old)this.flow && this.flow == new int[this.num][4];
(3)、* @EFFECTS: (\exist Path p from start to end; p is the shortest
* && ((\all Path t from start to end; t is the shortest)
* ==> sum(t; start to end; flow of edges) >= sum(p; start to end; flow of edges)
* )
* )
* ==> this.path == p;
*/
改为：
* @EFFECTS: (\exist Path p from start to end; p is the shortest
* && ((\all Path t from start to end; t is the shortest)
* ==> sum(t; start to end; flow of edges) >= sum(p; start to end; flow of edges)
* )
* )
* ==> this.path == p;
* (\all Path p from start to end; p is the shortest
* && ((\all Path t from start to end; t is the shortest)
* ==> sum(t; start to end; flow of edges) == sum(p; start to end; flow of edges)
* )
* )
* ==> this.path == the last found p;
*/
(4)、* @EFFECTS: this == new Server;
改为：
* @EFFECTS: this.list != null && tihs.taxis !=null && this.cpt !=null && (\all Taxi t; Main.taxiList.contains(t)) ==> t.sv == this;
(5)、* @EFFECTS: (\all int i,j; 0<=i<this.num,0<=j<this.num; \exist path(i,j)) ==> \result ==true;
改为：
* @EFFECTS: (\all int i,j; 0<=i<this.num,0<=j<this.num; i==j || \exist path(i,j)) ==> \result ==true;
五、功能bug和规格bug交互关系
|
作业 |
类名/方法名 |
功能bug数 |
规格bug数 |
|
第九次 |
Taxi/run |
0 |
1 |
|
Taxi/shortPath |
1 |
0 |
|
|
第十次 |
fileHandler/readFile |
1 |
1 |
|
Server/run |
1 |
0 |
|
|
第十一次 |
Road/openRoad |
1 |
0 |
六、感想体会
回顾这三次作业，第一次要写规格的时候确实不知从何下手，布尔表达式的运用也不够熟练。第二次修改时发现了很多不太合理的地方，思路逐渐清晰了。我个人感觉程序设计和规格的描述是相辅相成的东西，我从开始的先写代码再硬着头皮凑上几句规格到后来先大致思考好了前置后置条件，再来编写程序，补全规格的时候可能又会意识到自己程序里面冗余的地方，继而改进优化。
但就目前看来，我还是有很多不足的地方，只能说是有了一个规格化设计的意识，但是具体做的还没那么完善，也会遇到很多问题，还是应该再加强学习。
原文：https://www.cnblogs.com/susie-sun/p/9111360.html