规格化历史
规格化的出现源于统合各个厂商各有各的格式而产生出的问题。其优势在于可以对事物给出一个明确的标准，从而减小出错的几率。
规格Bug
| repOK有效信息不足 | 平均1行 |
| Effects不完整 | 平均20行 |
产生原因
主要原因是部分规格没有写完整，如 repOK 没有完整地考虑到所有的不变量，部分线程的 Effects 没有写出。
前置和后置条件的不好写法
前置条件
| 不好写法 | 好的写法 |
| a 有序 | for all i in [0,len(a)-1) ==> a[i]<=a[i+1] |
| b 属于 a | exist c in a ==> b == c |
| a.x != 0 | a != null && a.x != 0 |
| a==b | a != nulll && a == b |
| x<100 | 0<=x<100 |
后置条件
| 不好写法 | 好的写法 |
| 返回值有序 | for all i in [0,len( esult)-1) ==> esult[i]<= esult[i+1] |
| b 属于返回值 | exist c in esult ==> b == c |
| esult.x != 0 | esult != null && esult.x != 0 |
| esult==b | esult != nulll && a == b |
| esult<100 | 0<= esult<100 |
聚集关系
| 方法 | 功能bug | 规格bug |
| repOK() | 0 | 1 |
| 线程相关方法 | 0 | 1 |
| Taxi.wait() | 1 | 0 |
| Inputprocessor.process() | 1 | 0 |
体会
通过这三次作业，我体会到了规格的重要性，它就像是一个指引我们代码编写方向的航标，只要在一开始就设计好了规格，编写代码是一件再简单不过的事。而如果将这些步骤倒过来做，那么写代码时就容易无从下手，导致代码质量低下。