当熬过了一次次黑暗，迎接我们的却是被扣的惨不忍睹的JSF
┭┮﹏┭┮
一、总结调研
规格的历史
传统科学的特点是发现世界，而软件的特点是构造世界。软件的最底层就是0，1，两个离散的值。程序设计语言的三次分离使软件技术产生了飞跃。
程序设计的演变大致可以分成以下三个过程：
1.20世纪60年代以前，计算机刚刚投入实际使用，软件设计往往只是为了一个特定的应用而在指定的计算机上设计和编制，采用密切依赖于计算机的机器代码或汇编语言，软件的规模比较小，很少使用系统化的开发方式，此时的代码更多的是私人性质的，满足个人要求的程序
2.60年代中期，大容量、高速度的计算机出现，随之出现的是代码量急剧提升，复杂度急剧增长、程序可靠性问题突出的问题。结果化程序设计随之提出，它要求程序设计时以模块为单位，每个模块专职自己的工作，而要在模块间交流，在开发者和用户，开发者和开发者之间交流，就只需要相应接口即可；
3.80年代，面向对象的设计开始在业界大行其道，相比于单纯的结构化设计，面向对象的设计从审视问题的角度上就有了差异，程序发生了从围绕“行为”执行到围绕“客体”执行的变化，随之而来的，就是封装性地提高，可重用性的提高，可以说，面向对象进一步实现了结构化设计，是结构化设计更进一步的实现。说明是类型定义和操作描述，体是操作的具体实现。（具体的例子就是C++,Java等面向对象语言的类说明与类实现的分离。）解决方案设计只关注说明，实现时引用或者设计体。体的更改、置换不影响规格说明，保证了可移植性。支持多机系统，但要同样环境。此时产生了划时代的面向对象技术。在结构化越加明确的同时，开发者与设计者，开发者与用户，开发者与开发者之间的交流，就需要“抽象”来实现，因为彼此间不需要关心对方的实现方法，而只需要知道这个模块的接口有什么要求，会改什么，能做什么就行。通过规格化抽象，我们就能将这种交流变得高效，同时也降低了维护和修改的难度。
4.基于构件开发：标准化的软件构件如同硬件IC，可插拔，使用者只用外特性，不计内部实现。Web Services：软件就是服务。分布式，跨平台，松耦合。
为什么规格很重要？
这三次分离中的第二次就是OO课程要求我们去做的，也是面向对象的精髓。在大型项目的开发中，单个项目不可能由一个人完成。多人协作共同完成任务就意味着不仅仅需要知道自己的代码做了什么，还要知道别人的代码做了什么。自己的代码是自己写出来的，具体怎么实现，使用了什么样的数据结构，使用了什么样的算法，当然知道自己的程序会对什么产生影响，需要什么样的输入 。假设有个人写了一个方法，写好了，实现了，于是，他交了这份代码上去，你要使用这个方法，一看，这什么**玩意。花了时间适应了代码风格，知道要干嘛之后，写自己的代码进行测试，一测，bug，找了半天，发现是他和你的代码对于某个变量能不能修改有冲突。浪费了很长时间，再交给上面。。恶行循环。于是，规格的诞生可以说是拯救了这个局面。拿到代码，看前置条件，副作用，后置条件，就很清晰，永无bug（当然是不可能的）。
软件工程行业代码也越来越复杂，多人协作是必不可少，规格在我看来是代码风格的调和剂，多人项目运作的润滑油。
二、规格bug及分析
第九次作业
| Effects不完整 | 92行：@EFFECTS: true ==> (parse the input); |
| Effects内容为实现算法 | 34行：@EFFECTS: true ==> (read the map); |
>这次作业两个bug的产生一是因为方法写的太过冗杂，导致Effects描述功能并不能描述的很是详尽，二是一些比较奇怪的方法由于个人能力有限只能用自然语言去尽量的描述，比如上面的对于读取地图的方法。
第十次作业
| Effects不完整 | 77行：@THREAD_EFFECTS: this.MS; |
| Modified不完整 | 59行：@MODIFIES: System.out,this.output,this.rl;缺少 |
>这次的bug和上次基本一样吧。也就是方法没有设计得很好。从第九次作业开始，很多的方法都是沿用的之前的作业，而之前已经写好的方法重新加上规格会导致有一些本末倒置的意味，并且课下发放的JSF并不能完全解决我们对于规格的理解，所以在编写程序规格时难免出现一些问题，归结原因还是不熟练以及缺乏类似的思想。至于新增的方法没有写JSF还是因为自己先写了方法本身，而非老师说的先写规格再写代码。总之规格写的很迷就是了。
第十一次作业
无JSF bug
三、不好的规格写法及改进
前置1：赋值“=”应该改为“==”
/**
*@REQUIRES: s!=null,s=TAKING||s=WAITING||s=SERVING||s=STOP;
*@MODIFIES: this.status;
*@EFFECTS:
* status==s;
*/
public void SetStatus(TaxiStatus s){
this.status=s;
}
//正确写法
/**
*@REQUIRES: s!=null,s==TAKING||s==WAITING||s==SERVING||s==STOP;
*@MODIFIES: this.status;
*@EFFECTS:
* status==s;
*/
public void SetStatus(TaxiStatus s){
this.status=s;
}
前置2：前置条件必须为布尔表达式
/**
* @REQUIRES: index is in 0-100;
* @MODIFIES:this.index;
* @EFFECTS: this.index == index;
*/
public TaxiCar(int index) {
this.index = index;
}
//正确写法
/**
* @REQUIRES: 0<=index<100;
* @MODIFIES:this.index;
* @EFFECTS: this.index == index;
*/
public TaxiCar(int index) {
this.index = index;
}
前置3：直接写null不判断对象存在与否
/**
* @REQUIRES: None;
* @MODIFIES: this.req; this.position;
* @EFFECTS: this.req == req; this.position == position;
*/
public Record(Request req, Point p) {
this.req = req;
this.position = p;
}
//正确写法
/**
* @REQUIRES: req != null && p != null;
* @MODIFIES: this.req; this.position;
* @EFFECTS: this.req == req; this.position == position;
*/
public Record(Request req, Point p) {
this.req = req;
this.position = p;
}
前置4：对于数字类型范围判断遗漏或错误
/**
*@REQUIRES:id!=null;
*@EFFECTS:
* \result==squad[id];
*/
public Taxi get(int id){
return this.squad[id];
}
//正确写法
/**
*@REQUIRES:id!=null，0<=id<=99;
*@EFFECTS:
* \result==squad[id];
*/
public Taxi get(int id){
return this.squad[id];
}
前置5：由于粗心缺少括号引起的逻辑错误
/**
* @REQUIRES: req != null && index >= 80 || index < 0;
* @MODIFIES: this.req; this.index;
* @EFFECTS: this.req == req; this.index;
*/
public Record(Request req, int index) {
this.req = req;
this.index = index;
}
//正确写法
/**
* @REQUIRES: req != null && (index >= 80 || index < 0);
* @MODIFIES: this.req; this.index;
* @EFFECTS: this.req == req; this.index;
*/
public Record(Request req, int index) {
this.req = req;
this.index = index;
}
后置1：尽量不要使用自然语言（与前置不同，不是必须的）
/**
* @REQUIRES: req != null;
* @MODIFIES: None;
* @EFFECTS: 判断起始点与目标点是否为同一个点
*/
public boolean samedest(Request req) {
if(req.getSrc().equals(req.getDst())) {
return true;
}
else
return false;
}
//正确写法
/**
* @REQUIRES: req != null;
* @MODIFIES: None;
* @EFFECTS: (req.getSrc() == req.getDst()) ==> \result == true;
* (req.getSrc() != req.getDst()) ==> \result == false;
*/
public boolean samedest(Request req) {
if(req.getSrc().equals(req.getDst())) {
return true;
}
else
return false;
}
后置2：缺少程的规格
/**
*@MODIFIES: System.out;
*@EFFECTS:
* true==>(do the things below in an endless loop)==>(wait())==>(dispatch());
*/
public void run(){
while(true){
try {
synchronized(this.MS){
this.MS.wait();
this.dispatch();
}
//System.out.println(System.currentTimeMillis());
} catch (Throwable e) {
System.out.println("Error in Scheduler");
System.exit();
}
}
}
//正确写法
/**
*@MODIFIES: System.out;
*@EFFECTS:
* true==>(do the things below in an endless loop)==>(wait())==>(dispatch());
*@THREAD_EFFECTS: this.MS;
*/
public void run(){
while(true){
try {
synchronized(this.MS){
this.MS.wait();
this.dispatch();
}
//System.out.println(System.currentTimeMillis());
} catch (Throwable e) {
System.out.println("Error in Scheduler");
System.exit();
}
}
}
后置3：未处理异常（没有说明）
public static int min (int[ ] a) throws NullPointerException, EmptyException
/**@ EFFECTS: \result == \min a;
*/
//正确写法
public static int min (int[ ] a) throws NullPointerException, EmptyException
/**@ EFFECTS: normal_behavior
\result == \min a;
(a == null) ==> exceptional_behavior (NullPointerException);
(a.length == 0) ==> exceptional_behavior (EmptyException);
*/
后置4：方法行数太多导致描述遗漏或无法描述
/**
*@MODIFIES: this.light,this.lightmap;
*@EFFECTS:
* Change the lights
*/
public void Change(){
for(int i=;i<;i++){
for(int j=;j<;j++){
if(Main.light[i][j]==){
Main.light[i][j]=;
guigv.lightmap[i][j]=;
Main.TG.SetLightStatus(new Point(i,j),);
}
else if(Main.light[i][j]==){
Main.light[i][j]=;
guigv.lightmap[i][j]=;
Main.TG.SetLightStatus(new Point(i,j),);
}
}
}
}
//正确写法
/**
*@MODIFIES: this.light,this.lightmap;
*@EFFECTS:
* (\all int i,j,k;0<=i,j<80,light[i][j]>0)==>
* ((light[i][j]==1)==>(light[i][j]==2&&lightmap[i][j]==1)&&(light[i][j]==2)==>(light[i][j]==1&&lightmap[i][j]==2));
*/
public void Change(){
for(int i=;i<;i++){
for(int j=;j<;j++){
if(Main.light[i][j]==){
Main.light[i][j]=;
guigv.lightmap[i][j]=;
Main.TG.SetLightStatus(new Point(i,j),);
}
else if(Main.light[i][j]==){
Main.light[i][j]=;
guigv.lightmap[i][j]=;
Main.TG.SetLightStatus(new Point(i,j),);
}
}
}
}
后置5：描述逻辑不正确或不准确
/**
* @REQUIRES : None;
* @MODIFIES : this.AskList;
* @EFFECTS : AskList.contains(ask);
*/
public synchronized void addAsk(Ask ask){
AskList.add(ask);
}
//正确写法
/**
* @REQUIRES : None;
* @MODIFIES : this.AskList;
* @EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;
*/
public synchronized void addAsk(Ask ask){
AskList.add(ask);
}
四、功能bug与规格bug的聚焦关系
| 作业次数 | 功能bug数 | 规格bug数 | 聚焦关系 |
| 第九次 | 2 | 2 | 无明显关系 |
| 第十次 | 7 | 2 | 无明显关系 |
| 第十一次 | 2 | 0 | 无明显关系 |
其实从bug数上根本看不出来在功能上和规格上的bug之间有什么明显的关系。但我确实比较倾向于一个好的规格，必然是一个代码行数比较少，而且功能单一且明确的方法所具备的。而这样的代码写出来在功能上的bug也十分容易被发现并改正。从整个程序的设计来考虑，当一个方法的规格复杂时，必然需要更多的篇幅和代码来进行实现，出现bug的几率也会越大。所以我们以后写代码一定要以规格来写代码。
五、心得体会
其实说关于设计规格和撰写规格的思路与体会也并没有什么特别的，因为我们在训练撰写规格是在以前写的方法的基础上去完善的。但是由于以前写的方法功能比较杂糅，而且个别方法特别长，所以并不是很好地去撰写一个比较标准的规格。我们也没有进行一个先写规格再根据规格写代码的训练，对于这方面我也没有经验。但是我还是觉的这方面的训练是十分有必要的。因为一个好的代码一定是可移植好维护的，而设计一个好的规格是写一个好的代码的基础。
最后希望大家都能善良一点，开心一点，共同迎接OO胜利的曙光咯~
