OO终于要结束了，开个心先
一、规格化设计
规格化设计的一个重要目的是为了将模块的功能，约束通过抽象和层次分类来表达清楚，方便用户与开发者的信息交流，与结构化设计有着密不可分的关系。
程序设计的演变大致可以分成以下三个过程：
1. 20世纪60年代以前，计算机刚刚投入实际使用，软件设计往往只是为了一个特定的应用而在指定的计算机上设计和编制，采用密切依赖于计算机的机器代码或汇编语言，软件的规模比较小，很少使用系统化的开发方式，此时的代码更多的是私人性质的，满足个人要求的程序
2. 60年代中期，大容量、高速度的计算机出现，随之出现的是代码量急剧提升，复杂度急剧增长、程序可靠性问题突出的问题。结果化程序设计随之提出，它要求程序设计时以模块为单位，每个模块专职自己的工作，而要在模块间交流，在开发者和用户，开发者和开发者之间交流，就只需要相应接口即可；
3. 80年代，面向对象的设计开始在业界大行其道，相比于单纯的结构化设计，面向对象的设计从审视问题的角度上就有了差异，程序发生了从围绕“行为”执行到围绕“客体”执行的变化，随之而来的，就是封装性地提高，可重用性的提高，可以说，面向对象进一步实现了结构化设计，是结构化设计更进一步的实现。说明是类型定义和操作描述，体是操作的具体实现。（具体的例子就是C++,Java等面向对象语言的类说明与类实现的分离。）解决方案设计只关注说明，实现时引用或者设计体。体的更改、置换不影响规格说明，保证了可移植性。支持多机系统，但要同样环境。此时产生了划时代的面向对象技术。在结构化越加明确的同时，开发者与设计者，开发者与用户，开发者与开发者之间的交流，就需要“抽象”来实现，因为彼此间不需要关心对方的实现方法，而只需要知道这个模块的接口有什么要求，会改什么，能做什么就行。通过规格化抽象，我们就能将这种交流变得高效，同时也降低了维护和修改的难度。
4.基于构件开发：标准化的软件构件如同硬件IC，可插拔，使用者只用外特性，不计内部实现。Web Services：软件就是服务。分布式，跨平台，松耦合。
程序设计语言的第二次分离催生了规格化设计的诞生，规格化优点很多，故得到了人们的重视。
二、自己所被报告的规格bug以及雷同的规格bug
第九次作业
| Effects不完整 | 77行：@THREAD_EFFECTS: this.MS; |
| Requires不完整 | 176行：@REQUIRES:id!=null; |
第十次作业
无规格bug
第十一次作业
| Modified不完整 | 59行：@MODIFIES: System.out,this.output,this.rl;缺少 |
| Effects逻辑错误 | 196行：String s=a+" "+b+" "+0； “=”应为“==” |
| 没有JSF | 有两个新增方法没写JSF |
三、产生BUG的原因
一方面是因为从第九次作业开始，很多的方法都是沿用的之前的作业，而之前已经写好的方法重新加上规格会导致有一些本末倒置的意味，并且课下发放的JSF并不能完全解决我们对于规格的理解，所以在编写程序规格时难免出现一些问题，归结原因还是不熟练以及缺乏类似的思想。至于新增的方法没有写JSF还是因为自己先写了方法本身，而非老师说的先写规格再写代码，至于Requires，Modified和Effects的不完整就纯属于自己的粗心大意。没有什么可辩解的，希望这几次作业能够培养自己以后写注释写规格的习惯，并且能够写的尽量简洁准确。
四、规格不好的写法和改进
1、不指定数据范围，单纯写null
1 /**
2 *@REQUIRES:id!=null;
3 *@EFFECTS:
4 * \result==squad[id];
5 */
6 public Taxi get(int id){
7 return this.squad[id];
8 } 对于id来讲除了不为null还应当满足内部条件，改进为：
/**
*@REQUIRES:id!=null，0<=id<=99;
*@EFFECTS:
* \result==squad[id];
*/
public Taxi get(int id){
return this.squad[id];
} 2、没有判断类型
/**
*@REQUIRES: r!=null;
*@MODIFIES: this.SRC,this.DST,this.status,this.WaitCount;
*@EFFECTS:
* SRC==r.GetSrc();
* DST==r.GetDst();
* status==TAKING;
* WaitCount==0;
*/
public void getOrder(Request r){
this.SRC=r.GetSrc();
this.DST=r.GetDst();
this.status=TaxiStatus.TAKING;
this.WaitCount=0;
} r不仅应当不为null，还应当是一个Request对象，改进为：
/**
*@REQUIRES: r!=null，r instanceof Request;
*@MODIFIES: this.SRC,this.DST,this.status,this.WaitCount;
*@EFFECTS:
* SRC==r.GetSrc();
* DST==r.GetDst();
* status==TAKING;
* WaitCount==0;
*/
public void getOrder(Request r){
this.SRC=r.GetSrc();
this.DST=r.GetDst();
this.status=TaxiStatus.TAKING;
this.WaitCount=0;
} 3、=应为==（布尔表达式）
/**
*@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;
} 4、逻辑优先级问题
@REQUIRES:num instanceof int&& num==1||num==3 @REQUIRES:num instanceof int&&（num==1||num==3） 5、描述粗糙
@REQUIRES:taxis instanceof Taxi[] 应细致描述，改进为：
@REQUIRES:\all int i;0<=i<taxis.length;taxis[i] instanceof Taxi 6、描述尽量不用自然语言
/**
*@MODIFIES: this.Shot;
*@EFFECTS:
* (\all int i,j,k;0<=i,j<80,0<=k<100,Shot[i][j][k]!=-1)==>(Shot[i][j][k]==-1);
*/
public void Clear(){
for(int i=0;i<80;i++){
for(int j=0;j<80;j++){
for(int k=0;k<100;k++){
if(this.Shot[i][j][k]!=-1){
this.Shot[i][j][k]=-1;
}
else{
break;
}
}
}
}
} 7、不写线程相关的规格
/**
*@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(0);
}
}
} /**
*@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(0);
}
}
} 8、过于简略
/**
*@MODIFIES: this.light,this.lightmap;
*@EFFECTS:
* Change the lights
*/
public void Change(){
for(int i=0;i<80;i++){
for(int j=0;j<80;j++){
if(Main.light[i][j]==1){
Main.light[i][j]=2;
guigv.lightmap[i][j]=1;
Main.TG.SetLightStatus(new Point(i,j),1);
}
else if(Main.light[i][j]==2){
Main.light[i][j]=1;
guigv.lightmap[i][j]=2;
Main.TG.SetLightStatus(new Point(i,j),2);
}
}
}
} /**
*@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=0;i<80;i++){
for(int j=0;j<80;j++){
if(Main.light[i][j]==1){
Main.light[i][j]=2;
guigv.lightmap[i][j]=1;
Main.TG.SetLightStatus(new Point(i,j),1);
}
else if(Main.light[i][j]==2){
Main.light[i][j]=1;
guigv.lightmap[i][j]=2;
Main.TG.SetLightStatus(new Point(i,j),2);
}
}
}
} 五、功能bug和规格bug的聚集关系
对于我个人的程序来讲，功能bug和规格bug其实没有什么聚集关系，但是这种情况出现的原因主要是因为是先写完的代码才写的规格，导致两个描述可能是不一致的，但是从整个程序的设计来考虑，当一个方法的规格复杂时，必然需要更多的篇幅和代码来进行实现，出现bug的几率也会越大。
| 作业次数 | 功能性bug | 规格bug | 功能bug分析 | 规格bug分析 | 相关性/聚集关系 |
| 第九次 | 2 | 信用越界/初始化缺失 | 缺少某些requires和effects | 无 | |
| 第十次 | 1 | 右转等灯了 | |||
| 第十一次 | 3 | LoadFile指令没有记录，出租车没有指定，真假时间混用出错， | =应为==，忘记某些规格 |
六、心得体会
首先对于JSF这块，有一些不明白为何不在课程刚刚开始的时候就进行训练，而在需求逐渐增加的这个时刻开始要求，大家往往面对着既要改需求，又要书写JSF的双重考验，不过从长远来看，规格训练是必要的，只不过我认为这个不应该作为互测中扣分的点。规格书写主观性很强，很多同学功能完成的很好却被扣了很多规格的分，像我这样的由于觉得自己规格写的不够好，写的也很煎熬，所以在测试他人的时候就没有太过严格，感觉差不多就没有扣分，但是没想到测试我的狠人连我JSF里少打了一个=都发现了，并且依次检查了我所有的Modified，唯一缺失的一个也被就出来了，我觉得这是否有些本末倒置了，不过既然是自己的确错了，就得认，但是当自己看到互测结果是一大堆规格的时候心里还是不舒服的，费了很大劲写的功能，能让自己的出租车跑很多请求，优化BFS算法，结果弄了半天输在了JSF上了。说实话最近几次的OO作业写起来不难，但是心情的确不太好。不过OO总算也要结束了，大家也该歇歇了，查BUG的戾气太重，变成线上查BUG线下约架了。可以增加一个互测加分环节，说出别人代码的一个优点，给测试者加一分，这样大家都很开心，整个六系会陷入互相吹捧互相赞美的大好环境中。既然那么多人为了分数，那开心点岂不是更好。