一、规格发展历史
从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-1986ones定义了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）
个人认为规格是对程序内容功能的最直接的描述，从而提高项目设计中小组的合作效率，使得不同的人拿到对方的程序时不必生硬地阅读代码而直接通过规格了解它的内容并应用它。规格撰写的目的应该是最直接地显示出程序的内容，而规格化的规格撰写本意应是使得这样的说明含义明确，在使用中我的使用实际上没有达到这一目的。
二、bug统计及分析
第9次作业被报告了两个bug，分别是jsf的REQUIRES内容不完整以及没有实现多条道路同时开关的功能。之后对于第一个bug进行了一小段补充，对于第二个bug进行了进一步的考虑，将大部分方法的需求重新思考，主要将对参数的需求补充了上去。
第10次作业和第11次作业没有被报告bug。
| 序号 | Bug类别 | 对应方法的代码行数 | 产生原因 |
| 1 | REQUIRES不完整 | 多个地方都有类似问题 | 过于疏忽，没有分别分析 |
三、不好的例子及改进
1、缺失要求
/**
* @REQUIRES:None;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
改进后：
/**
* @REQUIRES:this.loc!=null
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
2、未规定参数有效
/**
* @REQUIRES:this.loc!=null
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
改进后：
/**
* @REQUIRES:this.loc!=null,aim!=null;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
3、未要求参数范围
/**
* @REQUIRES:this.loc!=null,this.loc!=null,aim!=null;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
改进后：
/**
* @REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
4、使用了单等号，不形成布尔表达式
/**
@REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4|| st = 7;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
改进后：
/**
@REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4 || st == 7;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
5、对对象自身状态未进行约束
/**
@REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
改进后：
/**
@REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4,this.loc.inrange() == true;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
6、使用了过多自然语言
/**
@REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc is changed according to aim,gui status is set according to aim and st;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
改进后：
/**
@REQUIRES:this.loc!=null,this.loc!=null,aim!=null,this.aim.nears(this.loc),st < 4;
* @MODIFIES:this.loc,this.gui,this.direction;
* @EFFECTS:this.loc == aim;
*/
synchronized public void changestate(Mypoint aim, int st) {
略
}
四、由于三次作业中我只被报了两个bug且无法归结到具体方法，因此这里的聚集关系分析略。
五、设计和撰写规格的基本思路和体会
首先必须承认我的几次出租车程序实在第七次作业就已经写好的，因此规格是后来才补充上去的。在撰写规格时我对自己的程序重新阅读梳理了一遍，发现自己的各个类方法调用次数都是有限的，自己脑海中也能较快地就回想起各个方法调用时的情境，因此我的类方法一个很大的特点就是REQUIRES内容很少，对类对象的状态很少做要求，对输入也是只要有效就可以，在逻辑上对参数基本没有要求，因此这一块我的规格撰写十分简单。另外EFFECTS部分我的方法分为改变对象状态和完成运算判断两种方法，这些方法的EFFECTS在撰写的时候比较明确，不会产生很多的交叉，因此规格只要把方法的效果表述清楚即可。