一、规格化设计介绍
为什么人们会重视规格化设计。对软件所应满足的要求，以可验证的方式作出完全、精确陈述的文件。“规格说明”一词与其他工业产品的“规格说明书”有相似的含义。不过,在软件领域中,它已成为一个特定的技术用语。软件产品与使用环境之间的关系，软件产品内部各组成部分之间的接口往往十分复杂，并且在发展过程中软件产品要经历多次变换，以各种不同形式出现于不同的阶段。因此，对软件的各组成部分之间、各发展阶段之间的接口关系应当规定得十分准确。软件规格说明须用某种语言书写。自然语言的陈述中常存在歧义性，易引起误解。因而，最好使用人工语言或者人工语言与自然语言的混合形式书写软件的规格说明。这种语言就叫作规格说明语言。大型软件的规格说明往往十分冗长，因而希望这种语言易于用计算机处理，以便能用机器检查软件规格说明中有无遗漏或自相矛盾的地方。软件规格说明的内容可根据不同场合的需要而有所侧重。
二、规格bug分析
第九次作业
| 序号 | bug类型 | 代码行数 | bug说明 |
| 1 | Effects逻辑错误 | 3 | 有些EFFECTS用的=，有的忘写了 |
| 2 | 不符合JSF规范 | 3 | 对加锁方法忘写线程安全条件了 |
| 3 | Requires不完整 | 59 | 一个私有方法没有限定输入的范围 |
第十次作业
| 序号 | bug类型 | 代码行数 | bug说明 |
| 1 | 针对构造方法，初始状态RepOk为真 | 4 | 构造Map类调用RepOK方法为假，对RepOK方法理解有误，我的Map仅仅是构造好后其实是不能用的，需要等待其他类在后期做一些同步设置。 |
| 2 | 针对构造方法，初始状态RepOk为真 | 10 | 判断条件少打了一个！取反 |
| 3 | 针对构造方法，初始状态RepOk为真 | 10 | 判断条件少打了一个！取反 |
第十一次作业
| 序号 | bug类型 | 代码行数 | bug说明 |
| 1 | Modifies不完整 | 2 | 对修改的属性没有记录Modifies |
| 2 | Effects逻辑错误 | 9 | 构造100辆出租车，EFFECTS中，前30辆和后70辆应该是不同的，但是沿用了旧的EFFECTS，做的相同处理 |
| 3 | 针对构造方法，初始状态RepOk为真 | 0 | 新出租车缺少RepOK方法，因为我直接继承的旧方法。我认为这也是可以的，但是不够严谨 |
三、不好的规格写法列举
1、描述过于简单，没有触及到核心
/**
* @REQUIRES: request!=null;
* @MODIFIES: front, rear;
* @EFFECTS: front == \old(front) == null ? request : \old(front) && rear.link==request && rear == request;
* @THREAD_RQUIRES: None;
* @THREAD_EFFECTS: \locked(RQ);
*/
对参数request的约束不够精确，应改为
/**
* @REQUIRES: request.repOK();
* @MODIFIES: front, rear;
* @EFFECTS: front == \old(front) == null ? request : \old(front) && rear.link==request && rear == request;
* @THREAD_RQUIRES: None;
* @THREAD_EFFECTS: \locked(RQ);
*/
2、可以用形式化语言但是却用了自然语言
/**
* @REQUIRES: true;
* @MODIFIES: None;
* @EFFECTS: if every request is OK,return OK . Otherwise false;
*/
EFFECTS采用的自然语言，可以改为形式化语言，应改为
/**
* @REQUIRES: true;
* @MODIFIES: None;
* @EFFECTS: \all Request p;queue.contain(p)&&p.repOK==>\result==true;
* \exist Request p;queue.contain(p)&&p.reqpOK==false==>\result==false;
*/
3、自然语言和形式化语言混用
/**
* @REQUIRES: src.inmap()&&dst.inmap();
* @MODIFIES: None;
* @EFFECTS: \result == direction with mindistance and minflow;
*/
EFFECTS采用的自然语言和形式化语言混用，应改为
/**
* @REQUIRES: src.inmap()&&dst.inmap();
* @MODIFIES: None;
* @EFFECTS: \result == mindistance;
*/
4、自然语言不恰当
/**
* @REQUIRES: true;
* @MODIFIES: new File("result").mkdir(),everything;
* @EFFECTS: everything will change as design;
*/
everything太绝对了，应改为
/**
* @REQUIRES: true;
* @MODIFIES: something;
* @EFFECTS: something will change as design;
*/
5、私有方法不加前置条件
private int getMinFlow(int src, int dst)
/**
* @EFFECTS: \result == direction with mindistance and minflow;
*/
私有方法也需要做前置条件约束，应改为
/**
* @REQUIRES:0<=src<6405&&0<=dst<6405
* @EFFECTS: \result == direction with mindistance and minflow;
*/
四、规格bug与功能bug关系分析
第九次作业
功能bug：2
规格bug：3
| 序号 | 功能bug | bug原因 | 与规格bug联系 |
| 1 | 不能设置出租车状态 | 理解问题 | 无 |
| 2 | 读入地图不能过滤制表符 | 没判断制表符 | 无 |
第十次作业
功能bug：4
规格bug：3
| 序号 | 功能bug | bug原因 | 与规格bug联系 |
| 1 | 不按初始设置的最小流量走 | 未设置正确的初始流量值 | 无 |
| 2 | 右转等红灯 | 左右方向判反 | 无 |
| 3 | 左转未等灯 | 左右方向判反 | 无 |
| 4 | 红绿灯不会变色 | 调试时不小心注释掉了 | 无 |
第十一次作业
功能bug：1
规格bug：4
| 序号 | 功能bug | bug原因 | 与规格bug联系 |
| 1 | 出租车走一条边时间不为500 | 等灯条件判断错误 | 无 |
五、总结体会
我觉得写JSF很累，但是在以后的团队合作中，把JSF写好却是很有必要的。
我在写JSF时，首先先完成的代码，然后再根据代码添加JSF。requires根据参数设定一些限制，Modifies为代码中修改的属性或传入的对象，Effects则稍微详细地说明Modifies中记录的属性修改情况。
虽然这样弄反了顺序，应该先写JSF再根据JSF完成代码，但是结合我自己的实际编程情况来看，这样却会带来一些不必要的麻烦。因为JSF也算是程序事先设计的一部分，然而程序的事先设计是很难考虑全面的，很多问题是在编程的过程中暴露的，通常是在一些功能逻辑比较复杂的代码段发现需要修改之前的设计，这个时候很容易导致JSF需要连带修改，而JSF最终的样子取决于实际上代码的真正实现。
所以我认为，对于接口方面的JSF，需要事先详细的设计和考虑，但是也要预留缓冲的情况保证遇到问题时能做调整，一些普通的JSF方法并不一定需要事先定死，留有余地才有空间实现更好的设计。
写JSF很累是不容置疑的，特别是后置条件如果认真的用形式化语言描述甚至比方法还长。但是JSF并不是写给自己看的，而是写给别人看的，以后的团队工作中，无论分工多么精细明确，最终还是会涉及到代码整合。这时就需要互相了解代码，好的JSF有助于快速的理解对方的逻辑，对于大工程和大项目而言，简单的注释比起JSF还是不够的。