一.规格化设计的发展历史
在微软的官网上，我找到了一篇描述规格的文章Specification and Verification of Object-Oriented Software,其中说到：
A system for specifying, writing, and verifying programs has many components. One component is the programming language itself and the specification constructs it contains. In some cases, specifications are not part of the program, but are provided separately. Another component is the compiler, which generates executable code from the program. Yet another component is the program verifier, which itself can include a subcomponent that formalizes the semantics and proof obligations of the program, a subcomponent that generates logical formulas, called verification conditions, from the formalization, and a subcomponent, called the theorem prover, that analyzes the verification conditions and searches for proofs or counterexamples.
不得不承认的是，相比于代码本身，规格的确有更强的规范性和更好的概括性，能够在多人合作的工程中让大家保持应有的默契。
以本学期的另一门课程操作系统为例，我们需要对已有的代码进行补充，从而完成一个功能健全的微型操作系统，在每个函数的头部，就有类似规格的说明，以处理缺页中断的pgfault函数为例，其说明为：
/* Overview:
* Custom page fault handler - if faulting page is copy-on-write,
* map in our own private writable copy.
*
* Pre-Condition:
* `va` is the address which leads to a TLBS exception.
*
* Post-Condition:
* Launch a user_panic if `va` is not a copy-on-write page.
* Otherwise, this handler should map a private writable copy of
* the faulting page at correct address.
*/
有Overview,有前置条件，有后置条件，俨然一个不符合JSF语法规范的完整规格，也正是有了这些类规格的说明，才能使得同学们快速地明白函数的功能，需要满足的需求以及需要考虑的情况，从而完成功能的实现。从数百人互相独立地补充完成了功能一致的操作系统，就可以看出规格化设计的优势。
正如K. Rustan M. LEINO所言，一个系统并不是代码本身，它还应该包含规格、验证等许多其它部分。规格设计自有其强大的生命力，不过，根据单词是否拼错、是不是缺个括号、等号写成了双等于还是单等于来评价规格的优劣，恕我不敢苟同。
二.bug分析
我的九次代码作业公测均为全部通过，如下是我九次代码作业在互测中被报的bug数目统计：
可以看到，我的前七次作业成绩虽略有波动，但整体比较平稳。以第九次作业为过渡，我的bug数目获得了突飞猛进的进步，屡创历史新高度，这是为什么呢？
首先需要声明的是，我并没有满足前七次的成绩而停滞不前，安于现状。相反，在出租车系列作业中，我投入的时间更多，仅以规格的书写为例，对代码进行度量统计后发现，我一共使用了253个方法，规格书写过程中，需要对每个方法的调用关系、前置后置条件进行分析，虽然其中有getter/setter此类比较容易进行规格设计的方法，但也不乏出租车运行、最短路计算等比较复杂的方法，同时我使用了IDEA中的Live Template,把更多的时间留给了设计而非书写，仅以平均每个方法书写规格大概需要5分钟计，253个方法需要1265分钟（即21小时）。而实际上，由于书写过程中难免出现遗漏，还需要一遍又一遍地阅读进行检查。此时，我听见钟敲了一下，我只是刚刚完成了规格设计，还没有看ISSUE上有没有修改需求，然后开始代码的设计、实现以及反复测试。
那bug数激增究竟是为什么呢？
总结起来，其实我感觉经过前几次的训练，编程能力已经获得了较大提升，对多线程的使用更加得心应手，不会感到难以驾驭，对整个程序架构的设计也初步有了自己的风格，此外，我还在编程进行了如下尝试：
- 不再单纯使用synchronized进行多线程互斥，为了提高并发性，尝试使用了读写锁、volatile等多种操作，尽可能减少了阻塞。
- 在流量的动态更新中，为了缩短线程启动所需时间，引入了线程池newCachedThreadPool
- 在设计中尝试使用了抽象类和抽象方法，使得代码结构更加清晰
- 有意识地对每个类进行了封装，final和private修饰符增多
- 在出租车信息输出时借鉴了IFTTT中的SafeFile类，实现了文件写入的线程安全
那bug数激增究竟是为什么呢？
在经历了愤懑、无奈、失望和深刻地自我反省等一系列激烈的情绪变化之后。我只能说，前几次bug数目很少并不能说明我的代码写得多么好，后几次bug数目很多也不能说明我的代码写得多么糟。
那bug数激增究竟是为什么呢？
如果非要解释的话，可以用观察者偏见来说明。由于观察者个人的动机和预期不同，可以导致观察者对同一件事物的评论截然不同。观察者偏见就像一个过滤器，一些事情被视为是相关和重要的而获得注意，而另外一些则被视为无关和不重要的而被忽略。具体来说，在每次作业中，每个人都可以拿到两份代码，一份是自己的，一份是他人的。如果带有观察者偏见看自己的代码，可能会对自己的代码产生自信，许多本身很轻易应该检查出来的错误可能就会被忽视。而如果带有较深的观察者偏见看别人的代码，可能就会觉得这份代码非常糟糕，应该被找出许多bug才对。这也是在申诉阶段闹出了许多矛盾甚至笑话的根源。
而另一个经典的社会心理学实验斯坦福监狱实验可能更能说明这一问题。当被赋予了不同角色之后，一个人的行为可能会在不觉间发生变化。情景力量对人的行为的影响程度可能是不可估量的。在互评过程中，每个人都有两个角色，一个是被测试者，处于相对弱势，如果想要申诉成功一个bug，可能需要花费相当多的时间和口舌；而另一个则是测试者，如果想要保持已有的“成果”，就得“坚守阵地”，不为所动。大家就是在这两个角色中不断切换，不断改变自己的说话语气和行为方式。当然每个个体受角色和规则的影响程度可能是不同的，因此就会呈现出不同的测试者和被测者组合，导致了有的同学最终bug少，而有的同学最终bug多（像我）。
下面晒一下我被报的系列bug供大家赏玩，其中不乏一些新奇有趣的(不要有分支和错误类型对不上的错觉，它就是这么被报的)：
功能性bug
| 所属分支 | bug说明 | |
|---|---|---|
| 第九次 | 随机行驶时未选择流量最小边运行 | 出租车在随机行驶过程中掉头 |
| 出租车随机行驶规则不符合指导书要求 | gui打开很久以后出租车的分布不均匀 | |
| 第十次 | 出租车下一步即将：右拐 | 经过多步理论推导后可以从输出文件中计算出红绿灯变化周期，几个数据的计算存在误差 |
| 是否选择流量最少路径 | 设置初始流量，出租车向流量多的方向走 | |
| 初始设置状态问题 | 设置出租车为接单状态，出租车会停几秒再走 | |
| 判断同质请求 | 初始化文件里放置了700条相同请求，有两条没有判为同质 | |
| 第十一次 | 服务状态出租车参与抢单 | 初始化文件里放置了1000条请求，请求处理结果不是在控制台一瞬间输出的 |
规格bug
（有部分用简短语句实在描述不清的并没有在下列表格中体现）
| JSF错误种类 | 被报bug数目 |
|---|---|
| REQUIRES中使用了';'而非'&&' | 1 |
| ==写成了= | 3 |
| 写操作MODIFIES不应该为None | 1 |
| 加锁忘记在 @THREAD_EFFECTS:中体现 | 1 |
| 一个简单get方法忘记写规格 | 3 |
| 变量名拼错一个字母 | 1 |
| MODIFIES不完整 | 1 |
| REQUIRES不完整 | 3 |
| EFFECTS里出现了动词 | 1 |
| 可以用逻辑表达式但是使用了自然语言 | 1 |
三.分析自己规格bug产生的原因
心理学中，对于失败的归因可以分为内部归因和外部归因两个维度，归因风格的不同可以极大的影响个体的动机、心境和行为。鉴于许多同学在博客中已经进行了外部归因，我在这里暂且总结一下内因：
- 方法数目太多（当然这是一个原因，但并不是一个问题），导致书写规格的工作量大，容易出错
- 少部分方法存在先写代码，最后补规格的现象，因此可能漏掉前置条件或者后置条件
- 重构代码时忘记修改规格
- 检查不够细致，例如仔细检查两遍程序，结果还是把两个“==”错写成了“=”
- 对规格的具体要求没有反复确认，被报了bug以后才知道对文件的写操作必须写在MODIFIES里
四.前置条件和后置条件的不好写法
1.前置条件
/**
* @REQUIRES: next!=null && next.length>6400;
* @MODIFIES: next
* @EFFECTS: next记录root到des最短路径上每个点的后继结点
*
esult==(root到des的最短路径长度)
*/
===============================================================================
/**
* @REQUIRES: next!=null && next.length>6400 && 0<=root<6400;
* @MODIFIES: next
* @EFFECTS: next记录root到des最短路径上每个点的后继结点
*
esult==(root到des的最短路径长度)
*/
/**
* @REQUIRES: 0 <=id< 100 && credit>=0 && pos_x>=0 && pos_x<80 && pos_y>=0 &&pos_y<80;
* @MODIFIES: this.id;
* this.credit;
* this.pos_x;
* this.pos_y;
* this.sendInfo;
* this.state;
* @EFFECTS: this.id == id;
* this.credit == credit;
* this.pos_x == pos_x;
* this.pos_y == pos_y;
* this.sendInfo == new SendInfo(id,new Coordinate(pos_x,pos_y),new Req(),new Vector<ReceiveInfo>(),true);
* this.state 为state对应的状态
*/
=====================================================================================
/**
* @REQUIRES: 0 <=id< 100 && credit>=0 && pos_x>=0 && pos_x<80 && pos_y>=0 &&pos_y<80;
* @MODIFIES: this.id;
* this.credit;
* this.pos_x;
* this.pos_y;
* this.sendInfo;
* this.state;
* @EFFECTS: this.id == id;
* this.credit == credit;
* this.pos_x == pos_x;
* this.pos_y == pos_y;
* this.sendInfo == new SendInfo(id,new Coordinate(pos_x,pos_y),new Req(),new Vector<ReceiveInfo>(),true);
* (state==0)==>this.state = STATE.SERVICE;
* (state==1):this.state == STATE.RECEIVE;
* (state==2):this.state == STATE.WAIT;
* (state==3):this.state == STATE.STOP;
*/
public static void stay(long time)
/**
* @REQUIRES: None
* @MODIFIES: None
* @EFFECTS: None
*/
=========================================================================================
/**
* @REQUIRES:time>0;
* @MODIFIES: None
* @EFFECTS: None
*/
2.后置条件
/**
* @REQUIRES: lightmap!=null && lightmap.length>=WIDTH*WIDTH;
* @MODIFIES: System.out;
* @EFFECTS: normal_behavior
* (exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;(i,j) isn't crossroads) ==>
* (输出提示信息 && lightmap[i][j]= 0;)
* (exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;lightmap[i][j]!=0 && lightmap[i][j]!=1)==>
* exceptional_behavior(MyException);
*/
==============================================================================
/**
* @REQUIRES: lightmap!=null && lightmap.length>=WIDTH*WIDTH;
* @MODIFIES: System.out;
* @EFFECTS: normal_behavior
* (exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;(i,j) isn't crossroads) ==>
* (输出提示信息 && lightmap[i][j]= = 0;)
* (exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;lightmap[i][j]!=0 && lightmap[i][j]!=1)==>
* exceptional_behavior(MyException);
*/
private void doReceive(){
/**
* @REQUIRES: pos!=null;task!=null;next!=null;next.length>6400;
* @MODIFIES: cal_path;curr_time;task;next;state;
* @EFFECTS: (old(cal_path)==false && curr_time-task.getSend_time()>Time.go_cost)==>
* (curr_time == task.getSend_time()+(Time.go_cost-Time.granularity)+(Math.abs(random.nextInt())%Time.granularity));
*
* (old(cal_path)==false)==>
* (task.start_time==curr_time && next更新为起点到终点的最短路 && cal_path==true);
*
* (old(cal_path)==true && pos.equals(task.getPassenger_posi()))==>
* (task.getin_time==curr_time && task.getPass_receive().contains(passby) &&
* curr_time==old(curr_time)+Time.stop_cost && state==STATE.SERVICE && cal_path==false);
*
* (old(cal_path)==true && !pos.equals(task.getPassenger_posi()))==>
* (task.getPass_receive().contains(passby));
*/
===========================================================================================
/**
* @REQUIRES: pos!=null;task!=null;next!=null;next.length>6400;
* @MODIFIES: cal_path;curr_time;task;next;state;
* @EFFECTS: (old(cal_path)==false && curr_time-task.getSend_time()>Time.go_cost)==>
* (curr_time == task.getSend_time()+(Time.go_cost-Time.granularity)+(Math.abs(random.nextInt())%Time.granularity));
*
* (old(cal_path)==false)==>
* (task.start_time==curr_time && next==(The shortest path from the beginning to the end) && cal_path==true);
*
* (old(cal_path)==true && pos.equals(task.getPassenger_posi()))==>
* (task.getin_time==curr_time && task.getPass_receive().contains(passby) &&
* curr_time==old(curr_time)+Time.stop_cost && state==STATE.SERVICE && cal_path==false);
*
* (old(cal_path)==true && !pos.equals(task.getPassenger_posi()))==>
* (task.getPass_receive().contains(passby));
*/
五.按照作业分析被报的功能bug与规格bug在方法上的聚集关系
事实上，功能bug和规格bug在方法上着实没有呈现出什么聚集关系，就第十一次功能和规格bug数目1：14来看，他们的相关系数应该在0附近波动。
如下是三次作业中两种bug的占比：
六.总结体会
在第十一次作业中，我所拿到Readme有13页之长，在最后一页留了一首小诗。虽然我拿到质量好的代码一般是抱着学习的态度阅读的，并不在意是否能找出bug，但这首诗还是给了我一些触动。
在这次博客的结尾我也想把它送给诸位：
煮豆燃豆萁，
豆在釜中泣。
本是同根生，
相煎何太急？