OO第三次博客作业——规格
一、调研结果：
规格的历史：
传统科学的特点是发现世界，而软件的特点是构造世界。软件的最底层就是0，1，两个离散的值。
程序设计语言的三次分离使软件技术产生了飞跃
1950年代，第一次分离，主程序和子程序的分离程序结构模型是树状模型，子程序可先于主程序编写。通过使用库函数来简化编程，实现最初的代码重用。产生基本的软件开发过程：分析—设计—编码—测试，使大型软件系统的开发成为可能
1975—1980年代，第二次分离，规格说明（Spec）和体（body）的分离说明是类型定义和操作描述，体是操作的具体实现。（具体的例子就是C++,Java等面向对象语言的类说明与类实现的分离。）解决方案设计只关注说明，实现时引用或者设计体。体的更改、置换不影响规格说明，保证了可移植性。支持多机系统，但要同样环境。此时产生了划时代的面向对象技术。
1995—2000年代，第三次分离，对象使用和对象实现的分离
基于构件开发：标准化的软件构件如同硬件IC，可插拔，使用者只用外特性，不计内部实现。Web Services：软件就是服务。分布式，跨平台，松耦合。
软件工程行业代码也越来越复杂，多人协作是必不可少，规格在我看来是代码风格的调和剂，多人项目运作的润滑油。
二、功能与规格BUG：
但是还是想说明一下，自己在规格上的一些不足和功能上的一些不足。
| JSFbug | 原因 |
|---|---|
| 后置条件使用了较多的自然语言 | 因为部分方法在设计的时候没有设计好，行数较长，使用布尔表达式过于繁杂，有点嫌麻烦 |
| 副作用有几个函数存在问题，比如System.out缺失 | 这是我刚和同学交流时才发现的（捂脸）,刚开始的时候写了，但是JSF检查工具给我报wrong，我就一直没写emm |
功能上：
| 功能bug | 原因 |
|---|---|
| (前两次作业都存在，第11次作业修复)接客时正好处于请求起点时，车辆无法正常运行 | 属于状态机中的边界状况，在计算下一个到达位置的时候，判断的是下一个位置与起始点，忽略了边界情况 |
三、列举不好的写法和改进：
1 /** 2 * @REQUIRES: None; 3 * @MODIFIES: this.req; this.position; 4 * @EFFECTS: this.req == req; this.position == position; 5 */ 6 public Record(Request req, Point p) { 7 this.req = req; 8 this.position = p; 9 } 10 //正确写法 11 /** 12 * @REQUIRES: req != null && p != null; 13 * @MODIFIES: this.req; this.position; 14 * @EFFECTS: this.req == req; this.position == position; 15 */ 16 public Record(Request req, Point p) { 17 this.req = req; 18 this.position = p; 19 }
前置2：不判断值是否符合实际
/*** @REQUIRES: None;* @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：未使用布尔表达式
/*** @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;}
前置4：遗漏
/*** @REQUIRES: req != 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;} //正确写法 /*** @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;}
前置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 && 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;} //正确 /*** @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;}
后置2：使用自然语言
/*** @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;}
后置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：描述不准确
/*** @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);}
后置5：多线程规格
/*** @REQUIRES : None; * @MODIFIES : this.AskList;* @EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;*/public synchronized void addAsk(Ask ask){AskList.add(ask);} //正确 /*** @REQUIRES : None; * @MODIFIES : this.AskList;* @EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;* @THREAD_EFFECTS : \locked(Asklist);*/public synchronized void addAsk(Ask ask){AskList.add(ask);}
四、感想与体会：
我在扣别人JSF时候，还是比较松的，第一次报了两个问题比较严重的，后面两次就只报了一个方法遗漏了JSF的bug。我会随机挑选几个函数的JSF进行查看，看能否get到这个函数的意思，我觉得能够让很多人快速理解代码的作用而不是每一行看代码找方法的作用就是JSF的精华。
还是挺开心的，OO的代码作业终于也是结束了，三次作业在设计上虽然不是十分的满意，但还是完成了基本的任务。虽然有一个边界条件直到最后一次作业才解决（其实我在第10次作业就发现了这个bug，原因是提交之前想测试一下能不能编译通过，结果出现了bug，复现了几遍都失败了，但是已经没有了时间，仅仅是初步判定了bug的可能位置，后来确实是我想的地方出了问题）。
最后，我记得第九次作业测试我的老哥在最后一个公测点，写了，和谐六系，OO不易，与君共勉，当时很感动。然后第10次和第11次作业都遇到了好人（或者是摸鱼测试者）。怎么说呢，虽然感谢老哥给我送分，但是感觉自己的程序的bug也被隐藏了emmmm。其实自己在课下有时候也能听到一些同学对OO互测的抱怨，有佛系测试者，有对结果很不满，有想击溃对面心理防线的（害怕&&鄙视）,有恶意扣分获利的，怎么说呢，面向运气是一方面，课程的精髓有时候被掩盖了。引入公测是好事，虽然我是公测的受害者（为什么呢，因为第三次作业，格式上出了错误导致公测全WA，被判了无效，如果是后几次的测试模式，我觉得也就是一个BUG的事，不至于无效。也不是开脱，毕竟是自己不小心，甚至第四次作业临交前，对了十几遍输出害怕再无效。要说觉得很难受就是第四次作业的时候有同学甚至输出了调试信息，都没有判无效，觉得很不平emmmm）。
这句话真的很好，和谐六系，OO不易，与君共勉。一起走向未来，Code the world! Debug the world！
