规格化的出现源于统合各个厂商各有各的格式而产生出的问题。其优势在于可以对事物给出一个明确的标准，从而减小出错的几率。
| 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(\result)-1) ==> \result[i]<=\result[i+1] |
| b 属于返回值 | \exist c in \result ==> b == c |
| \result.x != 0 | \result != null && \result.x != 0 |
| \result==b | \result != nulll && a == b |
| \result<100 | 0<=\result<100 |
| 方法 | 功能bug | 规格bug |
| repOK() | 0 | 1 |
| 线程相关方法 | 0 | 1 |
| Taxi.wait() | 1 | 0 |
| Inputprocessor.process() | 1 | 0 |
通过这三次作业，我体会到了规格的重要性，它就像是一个指引我们代码编写方向的航标，只要在一开始就设计好了规格，编写代码是一件再简单不过的事。而如果将这些步骤倒过来做，那么写代码时就容易无从下手，导致代码质量低下。
原文：https://www.cnblogs.com/zhong-zihao/p/9112609.html