面向对象第三次总结性博客
规格化设计的发展和重要性
关于这个题目，搜寻好久无果。反倒是找到了一个有意思的东西。
有趣的问题
The specification of object-oriented and other pointer-based programs must be able to describe the structure of the program’s dynamically allocated data as well as some abstract view of what the code implements. The verification of such programs can be done by generating logical verification conditions from the program and its specifications and then analyzing the verification conditions by a mechanical theorem prover.
所以综合来看，代码的规格是用来从一个抽象视角描述代码的实现的，可以从理论上论证代码的正确性。一个好的规格也有利于多人合作，方便代码的维护。阅读其他同学的博客，我无意间发现了有一个同学也引用了这篇文章，挺巧合的。
规格在当今的工程中也很常见，举个例子，最近C++大作业要求分析一个工程代码，在网上浏览了很多代码之后，发现但凡大型的工程中都存在着合乎要求、不合乎要求的规格。我想这也可以从侧面反映规格在多人合作中的重要性。
我的规格bug与产生原因
第9次作业
| 规格bug类别 | 所属方法 | 代码行数 | 产生原因 |
|---|---|---|---|
| Modifies逻辑错误 | ClosableFlowSelector.AimSelect | 11 | 在道路选择器类中进行有向的道路选择时，可能会给出租车增加行使任务，这会修改Mission属性，但Modifies中未写明 |
| Effects不完整 | Taxi.addCredit | 3 | 给出租车增加信用的方法中，Effects未写明出租车信用的增加 |
| Effects逻辑错误 | Taxi.SetTaxi | 5 | 给出租车设置初始状态的方法中，后置条件里“\result”描述的为方法返回值，但却描述了方法执行后的效果 |
| Requires不完整 | InputHandler.InputJudge | 55 | 该方法会根据传入的字符床String s来判断格式，再产生请求，Requires里应要求s!=null，以避免在处理字符串时产生异常 |
第10次作业
| 规格bug类别 | 所属类或方法 | 类或方法的行数 | 产生原因 |
|---|---|---|---|
| 针对构造方法，初始状态repOK为真 | ClosableFlowSelector | 120 | ClosableFlowSelector类的RepOk要求Mission不为null,但是并没有在构造方法中创建Vector,因此导致构造一个ClosableFlowSelector类的对象并调用其repOk方法后，返回false |
| 对于一个方法，开始执行时假设repOK返回值为true | Main | 123 | Main中有public的属性taxi，但repOK中要求了taxi不为空，导致测试者new Main之后再设置taxi=null会使repOK返回false |
| 对于一个方法，方法做的修改不会修改repOK | Taxi | 366 | 对于Taxi类，repOK要求了Credits>=0，但在其addCredit（int n)方法，忘记在REQUIRES方法中要求n>0了，导致传入的参数为负数时会造成repOk返回false。 |
| Requires不完整 | Moitor.Compete | 8 | 这里与测试者产生了分歧，个人认为我的Requires是完备的，测试者并没有设计出相应的样例，“脑中模拟”了一个不可能存在的问题 |
| 对于一个方法，开始执行时假设repOK返回值为true | Map | 88 | Map中有public的属性map，但repOK中要求了map!=null，导致测试者new Map之后再设置map=null会使repOK返回false |
| Effects不完整 | ClosableFlowSelector.AimSelect | 13 | 第9次互测的遗留问题，我针对上次代码的规格bug在Modifies中做出了调整，不过测试者好像不太满意，认为Modifies与Effects应成对出现，于是有了此bug |
第11次作业
| 规格bug类别 | 所属类或方法 | 类或方法的行数 | 产生原因 |
|---|---|---|---|
| Requires不完整 | Index.equals | 3 | 这里忘记要求Index!=null了，是我写方法规格时产生的疏忽 |
| Requires逻辑错误 | RoadSelector.getIndex | 9 | 分歧点，这个方法中只有一个switch-case语句，测试者认为其中的default语句有违Requires逻辑，我对此持否定态度 |
| 针对构造方法，初始状态repOK为真 | VIPTaxi | 251 | 写repOK时产生的疏忽，在repOK中把一个构造方法中不会初始化的变量要求了!=null |
前置、后置条件的加强
- 前置条件 前置条件中最容易出现的问题就是不完整，下面列举出的这三次代码中的例子也都是对前置条件不完整做出的改进。
| 方法名 | 作用 | 修改前 | 修改后 |
|---|---|---|---|
| Monitor.Compete(Taxi taxi) | 判断出租车是否要参与抢单，若抢单，则把hasCompete[]置为真 | @REQUIRES : taxi!=null && hasCompete.length>=taxi.GetName; | @REQUIRES : taxi!=null && hasCompete.length>=taxi.GetName; |
| Monitor(Passenger p, Taxi[] taxis, BufferedWriter tofile) | 根据一些列条件初始化监视窗口 | @REQUIRES : p!=null && taxis!=null && tofile!=null && taxis.length==100; | @REQUIRES : p!=null && taxis!=null && taxis.length==100 && (\all int i; 0<=i<=99; taxis[i]!=null) && tofile!=null; |
| FlowSelector.FreeSelect(Index present) | 无视道路变化，在等待服务状态时选择行走方向 | @REQUIRES : present!=null; | @REQUIRES : present!=null && 0<=present.Row<=79 && 0<=present.Column<=79; |
| TrafficLight.GetLight(int i, int j) | 得到坐标(i,j)处的红绿灯状况 | @REQUIRES : 0<=i<=79 && 0<=j<=79; | @REQUIRES : 0<=i<=79 && 0<=j<=79 && this.light.size==80 && (\all int p; 0<=p<=79; light[p].size==80); |
| IndexNode(int Nodnum, int depth) | 用于形成一个链表的链结点类，每个链结点指向他的前驱 | @REQUIRES : 0<=Nodnum<=6399； | @REQUIRES : 0<=Nodnum<=6399 && 0<=depth<=6399;备注：结点深度的极端情况为6399，是可能的 |
- 后置条件 在我的代码中后置条件大篇幅使用了自然语言，下面例子中的1、2、4、5均是试图将自然语言转换成布尔表达式做出的尝试，例子3是后置条件不完整做出的改进。
| 方法名 | 修改前 | 修改后 |
|---|---|---|
| Monitor.Compete(Taxi taxi) | @EFFECTS : (the taxi will compete the passenger) ==> (rise a taxi's Credits and change this.hasCompete); | @EFFECTS : (!\old(this.hasCompete)[taxi.name] && inRange(taxi))==>(taxi.addCredit(1) && \new(this.hasCompete)[taxi.name]==true && \result==true); |
| Main.hasLaunch(Passenger p) | @EFFECTS : (p has not been launched) ==> (this.Currentrequest will contain p); | @EFFECTS : (\old(this.recentLaunch).contains(p) ==> \result==false) && (!\old(this.recentLaunch.contains(p) ==>( \new(this.recentLaunch).size==\old(this.recentLaunch).size+1 && \new(this.recentLaunch).contains(p)); |
| Taxi.addCredit(int n) | @EFFECTS : \result == (None); | @EFFECTS : \new Credits == \old Credits+n && \result == (None); |
| Map.haspath(Index x1, Index x2) | @EFFECTS : \result == (\exist edge between x1 and x2 in initial map); | @EFFECTS : (guigv.m.graph[x1.row*80+x1.column][x2.row*80+x2.column]==1 ==> \result==true) && (guigv.m.graph[x1.row*80+x1.column][x2.row*80+x2.column]!=1 ==> \result==false); |
| Passenger.equals(Passenger p) | @EFFECTS : \result==(this has same requests with p); | @EFFECTS : \result==(this.Location==p.Location && this.Destination==p.Destination); 备注:这里可以看出自然语言的歧义：相同要不要包括请求发出时间也相同，而布尔表达式则不会有这种二义性 |
功能bug与规格bug的关系
纵观三次测试：
| 方法名 | 功能bug数 | 规格bug数 |
|---|---|---|
| Taxi.run() | 1 | 0 |
| FileLoader.loadrequest() | 1 | 0 |
| FileLoader.loadtaxi() | 1 | 0 |
| FileLoader.loadlight() | 1 | 0 |
综上所述，功能bug和规格bug一点关系都没有，而且说起来这几个功能Bug也很可笑，大概就是和测试者对一些字眼上的要求出现了分歧，比如测试者要求出租车必须要可设置为接单状态和服务状态，比如对红绿灯初始化时给出的提示不满意，再比如在设置初始请求时指导书强行要求同时性等等。
我觉得功能bug和规格bug无关的主要原因如下：- 虽然老师要求先写规格再写代码，但是这几次作业都是继承在第7次作业的基础上的，大部分代码都已经写好了，再去写规格就显得是亡羊补牢一样的效果。所以对于我来说，写代码和写规格本身就是分开的，甚至这二者在作业里的存在一开始就是没有关系的。
- 对测试者而说，也是先测代码功能，再去挑规格错误，在挑bug的时候也是分开的操作。比如我这三次的测试者，显然先是面向issue找bug之后，再去评估一下自己可能被扣的分，进而转去挑几个规格bug平衡一下。再综合第一点，找到的规格bug如果和功能bug有关系的话，反倒成了一种巧合。
思考和体会
在博客的一开始，我提到说规格的重要性是在多人协作时体现，或是在代码的后期维护时方便他人理解用的。可能这次作业的周期不长，又是单人完成的，自己对自己代码有着足够的理解，所以这可能导致我没有体验到规格的重要性。不过这几次作业倒是体会过规格了，以后如果真的需要写规格的时候也应该不会发难，因为自己至少知道规格是个什么东西，大概要怎么写。
不过有着规格化的代码的好处我们是体验过的，最明显的特点就是在这学期的另外一门课程——操作系统中，在每一个函数中，都有着Overview,Pre-Condition和Post-Condition，通过这些，我们可以知道这个函数的作用，前置条件，和后置条件。这些规格对于我们补全代码时给了极大的帮助。在这几次实验课的时候，我们也经历了一下根据规格补全代码的过程。很明显，有了良好规格的代码是很容易阅读的，我们不用管这个代码和其他代码的前后逻辑关系，不用阅读其他代码，只针对需要更改的代码，读完规格之后再将其翻译成代码语言就好了。 综上所述，没有规格的代码就像没有灵魂的肉体一样，没有生机，虽然勉强可以存在，但一点交互性都没有，只能用来自娱自乐，供写者自己欣赏。而规格的重要性，正是提供了代码本身的“交互性”，既方便了自己，也方便了其他阅读、学习、修改这段代码的人。 好像现在大家对OO都有一点怨言，虽然我的心态也崩了，但是其实理性来看，这个课还是不错的。