调研，然后总结介绍规格化设计的大致发展历史和为什么得到了人们的重视
emmm为这个问题翻遍百度谷歌知乎也没有得到答案，那我就把自己认为最重要的两点简要说明一下吧，欢迎大家补充~
1、便于完成代码的重用交接。
乌鸡老师上课说到，一个代码被重用的频率越高，说明设计的水平越高。好的代码一定是为他人提供便利的。而这种便利也包括引用时的确定性，调用者可以按照自己的需求和这份代码规格对照，因此确定自己使用这个接口的安全性可靠性。并且，代码规格也说明了调用者可视范围内变量的变化情况，否则这种重用将是非常非常危险的。因此，规格和代码的贴合性也变得很重要。
2、便于程序员按照真正的意愿做好代码实现和测试。
编程语言毕竟是自然语言之外的第二种语言，人是按照思维生成的逻辑去构造代码实现的。而把要实现的内容完全放在脑子里没有进行仔细的分类梳理，在代码越来越复杂的情况下很容易产生疏漏，也就是实现有BUG。但测试也是按照代码逻辑产生惯性思维，所以很难找到思维漏洞的BUG。然后...然后你就变成了“我司雇来写专门BUG的程序员”，然后你就凉了。
但规格是一种思维强制，强迫你按照你的预想去实现、去测试（有点像BUG树的作用原理）、去分类，只要规格和实现完全一致，最初有思维漏洞或许可以降低检查难度到规格层。
按照作业，针对自己所被报告的规格bug以及雷同的规格bug（限于 bug树的限制，对手无法上报），列一个表格分析
| 规格BUG类别 | 每个出现所对应方法的代码行数 |
| modified不完整 | 78 |
| modified不完整 | 145 |
分析自己规格bug的产生原因
这两个JSFbug都出现在第九次作业，而且错误原因基本都一样。这次作业因为一些特殊原因完成的特别仓促，也没有进行检查测试。产生的主要原因当然有时间方面的原因，更重要的是这两个方法的确也比较长。
当然，我的JSFbug水平咋样我心里还是很有笔数的，用自然语言也比较多。只是碰上的同学都比较友好，水平不高也没有被针对，但在三次作业中，我每次都对JSF进行优化，存在的问题选五个在下面介绍。
分别列举5个前置条件和5个后置条件的不好写法，并给出改进写法
前置条件部分：
参数范围描述不准确
例1
修改前：
/**
* @REQUIRES:(\all int id;);
* (\all int X;);
* (\all int Y;);
* @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
* @EFFECTS: Set these variables to their initial values;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public CarInformation(int id,int X,int Y) {
this.carID=id;
this.carX=X;
this.carY=Y;
this.carCredit=0;//信用值0
this.carStatus=2;//等待服务状态
this.hasTask=false;//没有任务
this.now_request=null;
this.load_result=false;
// System.out.println("出租车信息初始化成功");
}
修改后：
/**
* @REQUIRES:(\all int id;0<=id<100);
* (\all int X;0<=X<80);
* (\all int Y;0<=Y<80);
* @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
* @EFFECTS: Set these variables to their initial values;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public CarInformation(int id,int X,int Y) {
this.carID=id;
this.carX=X;
this.carY=Y;
this.carCredit=0;//信用值0
this.carStatus=2;//等待服务状态
this.hasTask=false;//没有任务
this.load_result=false;
// System.out.println("出租车信息初始化成功");
}
例2
修改前：
/**
* @REQUIRES:(\all int carX2;);
* (\all int carY2;);
* (\all ArrayList<Vertex> nei_Lis;);
* @MODIFIES: None;
* @EFFECTS: \result==new_aim;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public int Find_WhenCase2(int carX2, int carY2, ArrayList<Vertex> nei_Lis) {//在等待状态寻找一条流量最小的道路
int min_flownum=100000000;
int new_aim=-1;
for(int i=0;i<nei_Lis.size();i++) {
int ID=nei_Lis.get(i).getID();
int index=transIndex(ID,carX*80+carY);
//System.out.println("进入循环，CARX CARY"+carX+" "+carY);
if((Flow_List[carX*80+carY][index].Get_open())&&(Flow_List[carX*80+carY][index].Get_Lastflow()<min_flownum)) {
min_flownum=Flow_List[carX*80+carY][index].Get_Lastflow();
new_aim=i;
}
}
return new_aim;
}
修改后：
/**
* @REQUIRES:(\all int carX2;0<=carX2<80);
* (\all int carY2;0<=carY2<80);
* (\all ArrayList<Vertex> nei_Lis;);
* @MODIFIES: None;
* @EFFECTS: \result==new_aim;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public int Find_WhenCase2(int carX2, int carY2, ArrayList<Vertex> nei_Lis) {//在等待状态寻找一条流量最小的道路
int min_flownum=100000000;
int new_aim=-1;
ArrayList<Integer> roadaim=new ArrayList<Integer>();
for(int i=0;i<nei_Lis.size();i++) {
int ID=nei_Lis.get(i).getID();
int index=transIndex(ID,carX*80+carY);
//System.out.println("进入循环，CARX CARY"+carX+" "+carY);
if((Flow_List[carX*80+carY][index].Get_open())&&(Flow_List[carX*80+carY][index].Get_Lastflow()<min_flownum)) {
min_flownum=Flow_List[carX*80+carY][index].Get_Lastflow();
roadaim.clear();
roadaim.add(i);
}else if((Flow_List[carX*80+carY][index].Get_open())&&(Flow_List[carX*80+carY][index].Get_Lastflow()==min_flownum)) {
roadaim.add(i);
}
}
Random random=new Random();
int begin=0;
int end=roadaim.size()-1;
new_aim=roadaim.get(random.nextInt(end - begin + 1) + begin);
return new_aim;
}
例3：
修改前：
/**
* @REQUIRES:(\all int x;);
* @MODIFIES: carX;
* @EFFECTS: carX==x;
* @THREAD_REQUIRES:\locked(this);
* @THREAD_EFFECTS: \locked();
*/
public synchronized void setcarX(int x) {this.carX=x;}
修改后：
/**
* @REQUIRES:(\all int x;0<=x<80);
* @MODIFIES: carX;
* @EFFECTS: carX==x;
* @THREAD_REQUIRES:\locked(this);
* @THREAD_EFFECTS: \locked();
*/
public synchronized void setcarX(int x) {this.carX=x;}
例4：
修改前：
/**
* @REQUIRES:(\all int i;);
* @MODIFIES: carStatus;
* @EFFECTS: carStatus==i;
* @THREAD_REQUIRES:\locked(this);
* @THREAD_EFFECTS: \locked();
*/
public synchronized void setcarStatus(int i) {this.carStatus=i;}
修改后：
/**
* @REQUIRES:(\all int i;i=0/1/2/3;);
* @MODIFIES: carStatus;
* @EFFECTS: carStatus==i;
* @THREAD_REQUIRES:\locked(this);
* @THREAD_EFFECTS: \locked();
*/
public synchronized void setcarStatus(int i) {this.carStatus=i;}
例5：
修改前：
/**
* @REQUIRES:(\all int beginX;);
* (\all int beginY;);
* (\all int endX;);
* (\all int endY;);
* (\all long request_time;);
* @MODIFIES: beginX;beginY;endX;endY;request_time;AreaX1 to AreaX4;AreaX1 to AreaX4;AreaY1 to AreaY4;
* @EFFECTS: Set these variables to their initial values;Create area;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public Request(int beginX,int beginY,int endX,int endY,long request_time) {
this.beginX=beginX;
this.beginY=beginY;
this.endX=endX;
this.endY=endY;
this.request_time=request_time;
CreateArea();
}
修改后：
/**
* @REQUIRES:(\all int beginX;0<=beginX<80;);
* (\all int beginY;0<=beginY<80;);
* (\all int endX;0<=endX<80;);
* (\all int endY;0<=endY<80;);
* (\all long request_time;request_time>=0;);
* @MODIFIES: beginX;beginY;endX;endY;request_time;AreaX1 to AreaX4;AreaX1 to AreaX4;AreaY1 to AreaY4;
* @EFFECTS: Set these variables to their initial values;Create area;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public Request(int beginX,int beginY,int endX,int endY,long request_time) {
this.beginX=beginX;
this.beginY=beginY;
this.endX=endX;
this.endY=endY;
this.request_time=request_time;
CreateArea();
}
后置条件：
主要是自然语言描述以及没有对输入非法参数的情况描述
例1：
修改前：
/**
* @REQUIRES:(\all int id;0<=id<100);
* (\all int X;0<=X<80);
* (\all int Y;0<=Y<80);
* @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
* @EFFECTS: Set these variables to their initial values;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public CarInformation(int id,int X,int Y) {
this.carID=id;
this.carX=X;
this.carY=Y;
this.carCredit=0;//信用值0
this.carStatus=2;//等待服务状态
this.hasTask=false;//没有任务
this.load_result=false;
// System.out.println("出租车信息初始化成功");
}
修改后：
/**
* @REQUIRES:(\all int id;0<=id<100);
* (\all int X;0<=X<80);
* (\all int Y;0<=Y<80);
* @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
* @EFFECTS: this.carID==id;this.carX==X;this.carY==Y;this.carCredit==0;this.carStatus==2;this.hasTask==false;this.load_result==false;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public CarInformation(int id,int X,int Y) {
this.carID=id;
this.carX=X;
this.carY=Y;
this.carCredit=0;//信用值0
this.carStatus=2;//等待服务状态
this.hasTask=false;//没有任务
this.load_result=false;
// System.out.println("出租车信息初始化成功");
}
例2：
修改前：
/**
* @REQUIRES:(\all Flow_Count fl;);
* (\all CarInformation[] cars_info;);
* (\all Request_List list;);
* @MODIFIES: flowlist;cars_info;list;
* @EFFECTS: Set these variables to their initial values;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public MakeMap(Flow_Count fl,CarInformation[] cars_info,Request_List list,TaxiGUI g) {
this.flowlist = fl;
this.cars_info=cars_info;
this.list=list;
this.gui=g;
}
修改后：
/**
* @REQUIRES:(\all Flow_Count fl;);
* (\all CarInformation[] cars_info;);
* (\all Request_List list;);
* @MODIFIES: flowlist;cars_info;list;
* @EFFECTS: this.flowlist == fl;
this.cars_info==cars_info;
this.list==list;
this.gui==g;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public MakeMap(Flow_Count fl,CarInformation[] cars_info,Request_List list,TaxiGUI g) {
this.flowlist = fl;
this.cars_info=cars_info;
this.list=list;
this.gui=g;
}
例3：
修改前：
/**
* @REQUIRES: A file with the correct format and content;
* @MODIFIES: The neighbor‘s sequence of vertices and the value of the adjacency matrix;
* @EFFECTS:Convert the values in a file to node connections;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public void CreateMap() {//根据文件创建地图
}
修改后：
/**
* @REQUIRES: A file with the correct format and content;
* @MODIFIES: The neighbor‘s sequence of vertices and the value of the adjacency matrix;
* @EFFECTS:for(\all char c;c in file）
(c==‘1‘)==>road is opened;
(c==‘0‘)==>road is closed;
(!((c==‘0‘)&&(c==‘1‘)))==>system.exit(0);
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public void CreateMap() {//根据文件创建地图
}
例4：
修改前：
/**
* @REQUIRES: (\all int id;);
* @MODIFIES: System.out;
* @EFFECTS: find taxi by id;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public void checkBYcarID(int id) {// 通过汽车ID查询
if (id >= 100) {
System.out.println("ID越界，查询失败");
return;
}
FileWriter fw;
File printFile = new File(String.format("e://taxi3.txt",id));
if (!printFile.exists()) {
try {
printFile.createNewFile();
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
try {
fw = new FileWriter(printFile, true);
@SuppressWarnings("resource")
PrintWriter pw = new PrintWriter(fw);
CarInformation info = car_list[id];
System.out.println("查询时刻(100ms为基本单位):" + (long) System.currentTimeMillis() / (long) 100);
pw.println("查询时刻(100ms为基本单位):" + (long) System.currentTimeMillis() / (long) 100);
pw.flush();
System.out.println("出租车当前坐标:(" + info.getcarX() + "," + info.getcarY() + ")");
pw.println("出租车当前坐标:(" + info.getcarX() + "," + info.getcarY() + ")");
pw.flush();
String status = null;
switch (info.getcarStatus()) {
case 0:
status = "服务状态";
break;
case 1:
status = "接单状态";
break;
case 2:
status = "等待状态";
break;
case 3:
status = "停止状态";
break;
default:
status = "非法未知状态";
break;
}
System.out.println("出租车当前状态:" + status);
pw.println("出租车当前状态:" + status);
pw.flush();
} catch (IOException e) {
}
}
修改后：
/**
* @REQUIRES: (\all int id;);
* @MODIFIES: System.out;
* @EFFECTS: (0<=id<100)==>find taxi by id;
(!(0<=id<100))==>return;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public void checkBYcarID(int id) {// 通过汽车ID查询
if (id >= 100) {
System.out.println("ID越界，查询失败");
return;
}
FileWriter fw;
File printFile = new File(String.format("e://taxi3.txt",id));
if (!printFile.exists()) {
try {
printFile.createNewFile();
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
try {
fw = new FileWriter(printFile, true);
@SuppressWarnings("resource")
PrintWriter pw = new PrintWriter(fw);
CarInformation info = car_list[id];
System.out.println("查询时刻(100ms为基本单位):" + (long) System.currentTimeMillis() / (long) 100);
pw.println("查询时刻(100ms为基本单位):" + (long) System.currentTimeMillis() / (long) 100);
pw.flush();
System.out.println("出租车当前坐标:(" + info.getcarX() + "," + info.getcarY() + ")");
pw.println("出租车当前坐标:(" + info.getcarX() + "," + info.getcarY() + ")");
pw.flush();
String status = null;
switch (info.getcarStatus()) {
case 0:
status = "服务状态";
break;
case 1:
status = "接单状态";
break;
case 2:
status = "等待状态";
break;
case 3:
status = "停止状态";
break;
default:
status = "非法未知状态";
break;
}
System.out.println("出租车当前状态:" + status);
pw.println("出租车当前状态:" + status);
pw.flush();
} catch (IOException e) {
}
}
例5：
修改前：
/**
* @REQUIRES: (\all int status;);
* @MODIFIES: System.out;
* @EFFECTS: find taxi by status;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public void checkBYcarStatus(int status) {// 通过状态查询
if (!((status == 0) || (status == 1) || (status == 2) || (status == 3))) {
System.out.println("查询状态非法，查询失败");
return;
}
for (int i = 0; i < 100; i++) {
CarInformation info = car_list[i];
if (info.getcarStatus() == status) {
System.out.println("满足条件的出租车编号:" + info.getcarID());
}
}
}
修改后：
/**
* @REQUIRES: (\all int status;);
* @MODIFIES: System.out;
* @EFFECTS:
((status == 0) || (status == 1) || (status == 2) || (status == 3))==>find taxi by status;
(!((status == 0) || (status == 1) || (status == 2) || (status == 3))) ==>return;
* @THREAD_REQUIRES:
* @THREAD_EFFECTS:
*/
public void checkBYcarStatus(int status) {// 通过状态查询
if (!((status == 0) || (status == 1) || (status == 2) || (status == 3))) {
System.out.println("查询状态非法，查询失败");
return;
}
for (int i = 0; i < 100; i++) {
CarInformation info = car_list[i];
if (info.getcarStatus() == status) {
System.out.println("满足条件的出租车编号:" + info.getcarID());
}
}
}
按照作业分析被报的功能bug与规格bug在方法上的聚集关系
这里就不放表格了，因为测试的同学（虽然不知道是哪位仁兄）没有对我特别严格，而且实名承认自己是先写的代码后补的JSF，被报的JSFBUG和功能BUG没有对应关系，但不代表JSF的书写没有问题。
下面分析一下功能BUG中的问题，都截取自没有测试没有debug的第九次作业，共3个。
1、等待状态出租车走了回头路：
没有使用真正的随机，而是使用的循环break；使得每次选路都有一定规律，而且使用500ms清空一次流量的办法，数据访问一定的卡顿滞后。
2、等待服务状态20s未停止1s：
在输出和判断逻辑里使用了假时间，但初始为等待状态的出租车在假时间增加上有漏洞，不能按时增加到20s
3、测试接口没有正确实现：
这个Bug....实在是太低级了emmm 因为没有进行任何测试所以也没看出来。原因是逻辑表达式(!((status==0)||(status==1)||(status==2)||(status==3))) 写成了&&
所以，无论多忙，还是要好好测试，好好测试，好好测试！不然八成会凉。
归纳自己在设计规格和撰写规格的基本思路和体会
因为都是写好了代码才补的规格，所以谈不上什么太有价值的体会，只好把自己撰写jsf的主要方法简要谈一谈。
REQUIRES：我一般是光标点到变量上面，利用eclipse自带的阴影检查这个变量是方法内部声明的还是外部可见的。
MODIFIES：特别注意对非内部声明变量的赋值和return。
EFFECTS：一般就讲述什么条件下会得到什么样的返回结果。不要提及算法本身的过程。以及特别注意写明对非法输入参数的处理结果。
THREAD_RQUIRES\THREAD_EFFECTS：查看方法是否带锁。
总结
总之，OO课程虽然接近尾声了，一路遇到了很多很多友好的测试者感觉很幸运很感恩，但并不能因此掩盖自己的问题，我自己心里很明白作为一个预备程序猿和优秀的同学差距还是非常非常大，要学的东西还是太多，以后无论是自学还是正常学习课程都要多向身边比自己强的人谦虚请教，进步，永不止步。
原文地址：https://www.cnblogs.com/One-Is-All/p/9096702.html
时间： 2024-10-04 17:50:41