一、规格化设计的发展历史
从20世纪60年代开始，就存在着许多不同的形式规格说明语言和软件开发方法。在形式规格说明领域一些最主要的发展过程列举如下：
1969－1972 C.A.R Hoare撰写了"计算机编程的公理基础（An Axiomatic Basis for Computer Programming）"和"数据表示的正确性证明"两篇开创性的论文，并提出了规格说明的概念。
1974－1975 B.Liskow/S.N. Zilles和J. Guttag引入了"抽象数据类型"的概念。
1976 E.W. Dijkstra定义了"最弱前置条件"的概念
1977 R.Burstall和J.Goguen提出了第一个代数规格说明语言：Clear
1988 Standford的SRI开发了代数规格说明语言OBJ3
1980-1986 C.Jones定义了VDM语言，也就是维也纳开发方法。
1985－1992 牛津大学的程序研究小组开发了Z规格说明语言。与此同时BP研究室开发了称之为B方法的面向模型的规格说明语言。
1985－1993 在MIT和Digital SRC开发了代数规格说明语言Larch
从1991年开始，面向对象的形式规格说明语言开始发展，例如，Object-Z, VDM++, CafeOBJ等语言。
1996－2000年 在欧洲CoFI（Common Framework Initiative）项目资助下开发"统一"代数规格说明语言CASL(Common Algebraic Specification Language)
上述规格说明语言可以分为两大类：
l 基于代数和公理方法（Clear, OBJ, Larch, CafeOBJ）
l 基于模型的方法（VDM, Z, B, Object-Z）
(以上内容来自https://blog.csdn.net/jnucstan/article/details/1724259)
二、bug分析
| 功能bug | 规格bug | 有无联系 | |
| 第9次作业 | 0 | 3 | 无 |
| 第10次作业 | 1 | 1 | 无 |
| 第11次作业 | 未测试 | 未测试 | 未测试 |
第9次作业：
本次作业没有被报功能bug，但是被报了3个JSF的incomplete。第一个是对于已经加锁的方法，没有在JSF中说明出对应这一点，THREAD_REQUIRES和THREAD_EFFECTS全为None；第二个是访问队列时的下标i应该满足:\all int i;0<=i但是写成了None；第三个是大部分JSF使用自然语言书写。这次作业我刚刚接触JSF，对于规格化设计的理解还不够深入，因此犯了很多错误。感谢测试者一一为我指出，让我可以改正。
第10次作业：
本次作业我被报了1个功能bug，其实我觉得这个bug可有可无，测试者认为我的sleep(500)有问题，说这样的话会产生延迟，在sleep时应该用500减去延迟，可是我的输出全部用的是假时间，延迟多长对输出并没有影响，而且我在写代码时已经选择了避免延迟过大的写法，但是经过讨论之后，我觉得测试者说的也有道理，感觉他说的这种sleep方法应该是最合适的写法，所以最后我们商议的结果是把error改成incomplete。本次作业也被报了一个JSF的incomplete：有些简单逻辑也用了自然语言。其实我在上次作业被报incomplete之后已经把JSF改过一遍，但是唯独bfs这个类忘记改了，于是就被报了incomplete，这是吃了不仔细的亏。
第11次作业
写本次作业时，我认真修改了之前关于JSF的所有问题，把自然语言的使用频率降到最低，并把逻辑表达式检查了一遍，而且认真添加了新代码，写了设计文档，但是。。。测试者并没有给我测试。
三、规格bug产生原因的分析
一开始是看课件和Guideline看的不够认真，没有理解其精髓，而且时间紧迫，于是就大面积使用自然语言，而且逻辑写得不够仔细。之后对JSF进行了全面修改，但是因为少改了一个类的JSF而又被报了bug。最后一次作业我把JSF全部检查了一遍，虽然这次作业测试者没有给我测试，但是我觉得即使他测试了那也很难再挑出JSF的bug了。
四、规格的不好写法与改进
1、REQUIRES使用自然语言
/**@ REQUIRES:x和y都大于等于0且小于等于79; @ MODIFIES:None; @ EFFECTS:\result == lightstatus[x][y]; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:\locked(); @ */
改正：
/**@ REQUIRES:(x >= 0)&&(x <= 79)&&(y >= 0)&&(y <= 79); @ MODIFIES:None; @ EFFECTS:\result == lightstatus[x][y]; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:\locked(); @ */
2、忽略了必要的REQUIRES
/**@ REQUIRES:None; @ MODIFIES:None; @ EFFECTS:\result == queue[i].time; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:None; @ */
改正：
/**@ REQUIRES:(i >= 0)&&(i <= rear); @ MODIFIES:None; @ EFFECTS:\result == queue[i].time; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:None; @ */
3、EFFECTS使用自然语言
/**@ REQUIRES:(i >= 0)&&(i <= rear); @ MODIFIES:None; @ EFFECTS:返回queue[i].time; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:None; @ */
改正：
/**@ REQUIRES:(i >= 0)&&(i <= rear); @ MODIFIES:None; @ EFFECTS:\result == queue[i].time; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:None; @ */
4、没有概括异常情况
/**@ REQUIRES:None; @ MODIFIES:this; @ EFFECTS:(\old(this).get(index) !=null) ==> (this.size == \old(this).size-1) && (this.contains(\old(this).get(index))==false) && (\result==true); @ */
改正：
/**@ REQUIRES:None; @ MODIFIES:this; @ EFFECTS:(\old(this).get(index) !=null) ==> (this.size == \old(this).size-1) && (this.contains(\old(this).get(index))==false) && (\result==true); (\old(this).size ==0)==>exceptional_behavior(InvalidRemoveException); (index >=\old(this).size) ==> exceptional_behavior (InvalidRemoveException); (index < 0) ==> exceptional_behavior (InvalidRemoveException); @ */
5、EFFECTS写得不完整
/**@ REQUIRES:None; @ MODIFIES:queue,head; @ EFFECTS:\result == queue[head]; @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:None; @ */
改正：
/**@ REQUIRES:None; @ MODIFIES:queue,head; @ EFFECTS:(\result == queue[head])&&(head == \old(head) + 1); @ THREAD_REQUIRES:None; @ THREAD_EFFECTS:None; @ */
五、功能bug与规格bug在方法上的聚集关系
| 功能bug | 规格bug | |
| public long gettime(int i) | 0 | 1(REQUIRES不全，i有范围) |
| public synchronized void setflow(int x,int y,int i) | 0 | 1(已经加锁的方法，没有在JSF中说明出对应这一点) |
| 大多数run函数 | 0 | 1(自然语言) |
| Driver类的run函数 | 1(sleep延迟) | 1(自然语言，同上) |
可能是测试者测得不够认真，都没有给我找几个功能bug，几乎全是规格bug，因此很难看出功能bug与规格bug在方法上的聚集关系。
六、设计规格和撰写规格的基本思路和体会
1、基本思路
设计规格的时候要保证写得尽量简洁，做到每个方法只做一件事，这样在才能保证不会写出几百行长的超级方法，但是我的代码中仍然存在几百行长的超级方法，例如Driver类的run方法，因为当时写的时候没有要求规格，所以写得洋洋洒洒，后来也不好改了。写规格的时候要避免使用自然语言，例如队列的相关操作可以用contains和size等语言描述其EFFECTS。
2、体会
一定要先设计规格再写代码，训练自己设计规格和按照规格写代码的能力，先设计规格再写代码还能使代码写得更漂亮。