调研规格化设计
规格化设计的历史和发展进程网络上实在没有相关的资料.........
下面分析一下问什么得到人们的重视：
规格bug分析
| 规格bug | 对应方法的行数 |
| Effecets内容为实现算法 | 331 |
bug产生的原因：在EFFECTS中对于该方法的后置条件讨论不够充分，在不同情况下对于MODIFIES中的属性的改变情况说明过于模糊。这个方法中实现的是出租车带等待接单时车行走的方式，因为实现复杂无法通过形式化语言实现，所以后置条件讨论的不充分；对应的modifies属性的改变也是模糊的。
不好写法和改进写法
我的jsf写的确实不太好，因为有的方法实现的东西有很多，所以用的自然语言没有形式化语言；
1.我的出租车判断方向时：
返回值为-1不应该放入exception中
/**
* @ REQUIRES: None;
* @ MODIFIES: None;
* @ EFFECTS:
* normal_behavior:
* (x==n_x&&n_y>y)==>\result == 4;
* (x==n_x&&n_y<y)==>\result == 3;
* (y==n_y&&n_x>x)==>\result == 2;
* (y==n_y&&n_x<x)==>\result == 1;
* exception_behavior(Exception e):
* \result == -1;
*/
if(x==n_x&&n_y>y)
return 4;
else if(x==n_x&&n_y<y)
return 3;
else if(y==n_y&&n_x>x)
return 2;
else if(y==n_y&&n_x<x)
return 1;
return -1;
改进后
/** * @ REQUIRES: None;
* @ MODIFIES: None;
* @ EFFECTS:
* normal_behavior:
* (x==n_x&&n_y>y)==>\result == 4;
* (x==n_x&&n_y<y)==>\result == 3;
* (y==n_y&&n_x>x)==>\result == 2;
* (y==n_y&&n_x<x)==>\result == 1;
* (!(x==n_x&&n_y>y)&&!(x==n_x&&n_y<y)&&!(y==n_y&&n_x>x)&&!(y==n_y&&n_x<x)) ==> \result == -1;
*/
2.查询出租车信息时：
用自然语言写的很简略
/**
* @ REQUIRES: None;
* @ MODIFIES: None;
* @ EFFECTS:
* normal_behavior:
* 输出i号出租车的具体信息;
* exception_behavior(Exception e):
* do nothing;
*/
改进后
/**
* @ REQUIRES: None;
* @ MODIFIES: None;
* @ EFFECTS:
* normal_behavior:
* \result == "Time:\t"+System.currentTimeMillis()+"Station:\t("+t[i].x+","+t[i].y+")"+"Statics\t"+t[i].statics;
* exception_behavior(Exception e):
* do nothing;
*/
3.求处于某一状态的出租车的编号
用自然语言写的很简略
/**
* @ REQUIRES: None;
* @ MODIFIES: None;
* @ EFFECTS:
* normal_behavior:
* 输出处于statics状态的出租车编号;
* exception_behavior(Exception e):
* do nothing;
*/
改进后
/**
* @ REQUIRES: None;
* @ MODIFIES: None;
* @ EFFECTS:
* normal_behavior:
* (\all int i; 0<=i<100; (t[i].statics == statics) ==> /result == i;
* exception_behavior(Exception e):
* do nothing;
*/
4.判断是否还有路径的下一个结点
写法上还是不太好
/**
* @ Effects: \result == (cnt+1>=0 && cnt+1<=len-1) ==> true;
(cnt+1 <0 || cnt+1>len-1) ==> false;
*/
改进后
/**
* @ REQUIRES: None;
* @ MODIFIES: None;
* @ Effects: (cnt+1>=0 && cnt+1<=len-1) ==> \result == true;
* (cnt+1 <0 || cnt+1>len-1) ==> \result == false;
*/
5.返回路径的上一个节点时
写法上还是有自然语言
/**
* @ Requires: None;
* @ Modifies: None;
* @ Effects: \result == (cnt-1 >= A.arraylist.size() || cnt < 1) ? null : String of previous position
*/
改进后
/**
* @ Requires: None;
* @ Modifies: None;
* @ Effects: (cnt-1 >= A.arraylist.size() || cnt < 1) ==> \result == null;
* !(cnt-1 >= A.arraylist.size() || cnt < 1) ==> \result == A.arraylist.get(cnt);
*/
功能bug和规格bug在方法上的聚集关系
| 方法名 | 功能bug数 | 规格bug数 | |
| 第9次作业 | request | 1 | 0 |
| 第10次作业 | 无 | 1 | 0 |
| 第11次作业 | dispath | 2 | 1 |
在我的程序中，功能bug和规格bug没有体现出具体的聚集关系，但实际上他们是密切相关的，如果规格写不好的话很容易产生功能上的bug，相反规格写的易于理解，更加正规化的是可以大大降低产生功能bug的可能的；
自己在设计规格和撰写规格的基本思路和体会
这个jsf写起来确实非常的讨厌，消耗了大量的时间，可能会比写代码的时间用的还要多，但这个时间肯定是有所回报的，jsf是一个非常重要的东西。现在可能看不出来这个东西的重要性，但是当很多人在一起合作时，这个东西的重要性就体现出来了，为了和其他人进行交互你必须要别人看懂你的代码，而jsf就是一个非常好的让人看懂你代码的东西。同时jsf还能有助于你理清思路，让你减少功能性bug的出现。
总的来说，jsf是很枯燥，很无聊，但它是非常有用的，所以得好好写啊，不好好写就被扣分了(.jpg)！
原文：https://www.cnblogs.com/yangfenghaha/p/9095882.html