标签：ali 可维护性 nat als file har string 博客 思想
规格化设计的发展历史
20世纪60年代以前，软件刚刚诞生，规模较小，编写也没有规范，很少使用系统化的开发方式，通用性十分有限。
20世纪60年代末至20世纪70年代，随着计算机容量与运算速度的增大，软件代码量与规模得到扩大。程序在设计时更倾向于以模块为单位，每个模块专职自己的工作。在模块间交流，在开发者和用户，开发者和开发者之间交流时，只需要相应接口即可。
20世纪80年代，面向对象设计的流行带来了程序可重用性与封装性的提高，进一步实现了规构化设计，总而言之，规格化设计是一个自然而然的过程，随着自然语言和文档越来越难以满足程序员交流的需要，程序模块之间更关注接口的实现，有利于设计与功能的分离，也就更得到了人们的重视。
BUG分析
第九次作业
功能型BUG
| 方法名 | BUG数量 |
| main | 9 |
| WaitForService | 2 |
| 总计 | 11 |
规格BUG
| BUG说明 | BUG数量 |
| Incomplete-REQUIRES | 1 |
| Incomplete-MODIFIES | 1 |
| Incomplete-EFFECTS | 1 |
| ERROR | 1 |
| 总计 | 4 |
就第九次作业而言，规格BUG出现的原因是我没有领会到JSF在工程中的作用与意义所在，消极对待老师提供的学习材料，没有写JSF。第九次作业中的功能BUG与没有写JSF有一定的关系，以main函数而言，在没有写JSF的前提下，甚至采用了极其过程式的写法，导致main很冗余，如果写了JSF，会构思下每个方法要做什么，对清晰程序的结构有帮助。思路混乱的我写第九次作业时都在纠结自己代码里一个个.java文件要写什么方法，对程序使用与测试的考虑无从谈起，最终写出来的东西对测试者也十分不友好。在第十次和第十一次作业中，重构了代码，增加了JSF，没被报规格BUG和功能BUG。
5个不好的前置条件
1) this!=null
/** @REQUIRES: this != null; * @MODIFIES: none; * @EFFECTS : (\result == this.x*80+this.y); */
/** @REQUIRES: none; * @MODIFIES: none; * @EFFECTS : (\result == this.x*80+this.y); */
2) 不等号连用
/** @REQUIRES: 0 <= Dir <4; * @MODIFIES: this; * @EFFECTS : (\all int i;0 <= i <4 && DPC[i] < Min && DPC[i] > -1) ==>(Min == DPC[i]); * (\result == (DPC[Dir] == Min? true:false)); */
/** @REQUIRES: Dir >= 0 && Dir <4; * @MODIFIES: this; * @EFFECTS : (\all int i;0 <= i <4 && DPC[i] < Min && DPC[i] > -1) ==>(Min == DPC[i]); * (\result == (DPC[Dir] == Min? true:false)); */
3）忽视方法中的参数
void CreateLight(Map m) { /** @REQUIRES: this != null; * @MODIFIES: this; * @EFFECTS : (1 == 1); * (\all int i,j 0<=i<size,0<=j<size ) ==> (Light[i][j] == 0) ||(Light[i][j] == 1); */
void CreateLight(Map m) { /** @REQUIRES: this != nul && m! = null; * @MODIFIES: this; * @EFFECTS : (1 == 1); * (\all int i,j 0<=i<size,0<=j<size ) ==> (Light[i][j] == 0) ||(Light[i][j] == 1); */
4) 使用自然语言
void ReadLight(String path) { /** @REQUIRES: String path is the path of designated output file; * @MODIFIES: this; * @EFFECTS : (\all int i,j 0<=i<size,0<=j<size ) ==> Light [i][j] == line.charAt(j)-‘0‘; */
void ReadLight(String path) { /** @REQUIRES: path != null // String path is the path of designated output file; * @MODIFIES: this; * @EFFECTS : (\all int i,j 0<=i<size,0<=j<size ) ==> Light [i][j] == line.charAt(j)-‘0‘; */
5) 使用逗号代替 &&
/** @REQUIRES: x1< Size,Status == 0 || Status == 1; * @MODIFIES: System.out; * @EFFECTS : 1 == 1; */
/** @REQUIRES: x1< Size && (Status == 0 || Status == 1); * @MODIFIES: System.out; * @EFFECTS : 1 == 1; */
5个不好的后置条件
1)void方法 Effects不准确
void addString(String s) { /** @REQUIRES: none; * @MODIFIES: this; * @EFFECTS : (1 == 1); */ tep.ALS.add(s); }
void addString(String s) { /** @REQUIRES: none; * @MODIFIES: this; * @EFFECTS : (tep.ALS.size() == \old tep.ALS.size()+1) && (tep.ALS.contains(s)); */ tep.ALS.add(s); }
2)MODIFIES忽视System.out
/** @REQUIRES: none; * @MODIFIES: this; * @EFFECTS : (1 == 1); */
/** @REQUIRES: none; * @MODIFIES: this,System.out; * @EFFECTS : (1 == 1); */
3)构造方法只写(1 == 1)
TestThread(Taxi taxi[]){ /** @REQUIRES: (taxi != null && Num >=0 ); * @MODIFIES: none; * @EFFECTS : (1 == 1); */
TestThread(Taxi taxi[]){ /** @REQUIRES: (taxi != null && Num >=0 ); * @MODIFIES: none; * @EFFECTS : (this.t == taxi) && (this.CheckGap == 10000); // 初始每隔10秒查询一次 */
4)MODIFIES忽视this
TestThread(Taxi taxi[]){
/** @REQUIRES: (taxi != null && Num >=0 );
* @MODIFIES: none;
* @EFFECTS : (this.t == taxi) && (this.CheckGap == 10000); // 初始每隔10秒查询一次
*/
TestThread(Taxi taxi[]){ /** @REQUIRES: (taxi != null && Num >=0 ); * @MODIFIES: this; * @EFFECTS : (this.t == taxi) && (this.CheckGap == 10000); // 初始每隔10秒查询一次 */
5)MODIFIES为空时不统一 （....）
public String toString() { /** @REQUIRES: none; * @MODIFIES: none; * @EFFECTS : (\result == "Queue has "+num+" Element(s) "); */ return "Queue has "+num+" Element(s) "; }
Request getReq(int i) { /** @REQUIRES: 0 <=i < num; * @MODIFIES: null; * @EFFECTS : (\result ==r[i]); */ return r[i]; }
public String toString() { /** @REQUIRES: none; * @MODIFIES: none; * @EFFECTS : (\result == "Queue has "+num+" Element(s) "); */ return "Queue has "+num+" Element(s) "; }
Request getReq(int i) { /** @REQUIRES: 0 <=i < num; * @MODIFIES: none; * @EFFECTS : (\result ==r[i]); */ return r[i]; }
基本思路与体会
设计规格时要好好运用在学习中学到的模块化思想,注意方法的接口,从输出与输入上考虑,想想这个对象有什么行为,写好规格后发现不仅将代码的层次与结构优化了不少,而且也提升了程序的可维护性,看着一个个类和方法乖乖排好还是不错的
标签：ali 可维护性 nat als file har string 博客 思想
原文地址：https://www.cnblogs.com/pinex/p/9105897.html
