一、 规格发展历史
从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）
二、 bug统计及分析
|
功能bug |
规格bug |
是否有联系 |
|
|
第9次作业 |
2 |
1 |
无 |
|
第10次作业 |
5 |
0 |
是 |
|
第11次作业 |
3 |
0 |
是 |
分析：
规格化的BUG因为当时助教群里没有要求必须使用布尔表达式，所以当时使用了大量的自然语言，结果就被同学上报了一个complete这个以后会格外注意，不会在使用自然语言。至于功能上的BUG，有的能被同学测试出来我比较感激，有的就不能使我信服，在持续申诉中，同学指出的让我比较感激的BUG有关于信誉度的选择，应该选择信誉度最高的出租车，因为当时阅读指导书不够仔细，所以优先选择了距离比较近的其次是信誉度最高的，已做改正，还有是关于流量问题的，因为指导书变更了为道路总流量，而我只在每一步行走的时候选择了一个流量最小的道路，所以被报了一个BUG。让我比较迷的BUG在于被乱报关于红绿灯的问题，一下子报了好几个，就粘贴一段我的代码，说我写的有问题我觉得很是不能接受。希望这种现象会越来越少。
三、 规格举例
１、可以用布尔表达式但是使用了自然语言
/**@REQUIRES:
*@MODIFIES: this
*@EFFECTS: 如果taxi没有初始化就给taxi赋值
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
改进后：
/**@REQUIRES:
*@MODIFIES: this
*@EFFECTS: (init==true)==>(a=new taxi())
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
2、没有关于异常的信息
/** @REQUIRES:
*@MODIFIES:
*@EFFECTS:(a.contains(b))== >
esult ==b;
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
改进后
/**@REQUIRES:
*@MODIFIES:
*@EFFECTS: (a.contains(b))== >
esult ==b;
otherwise==>NoSuchelement
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
3、直接在effect里粘贴代码
/**@REQUIRES:
*@MODIFIES:
*@EFFECTS:(taxi!=null && requelist!=null)
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
改进后:
/**@REQUIRES:
*@MODIFIES:
*@EFFECTS:(taxi!=null && requelist!=null)==>
esult=true
otherwise==> esult=false;
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
4、前置条件、后置条件不准确。
/** @ REQUIRES: r!=null
@ MODIFIES: this
@ EFFECTS: RL[len++]=r
@ THREAD_REQUIRES:
@ THREAD_EFFECTS:
@ */
改进后:
/** @ REQUIRES: r!=null
@ MODIFIES: this
@ EFFECTS: r.repOK()==true ==> (RL[len++]==r) && (RL.contain(r)==true);
@ THREAD_REQUIRES:
@ THREAD_EFFECTS:
@ */
四、 聚焦关系
只被抱了自然语言的描述，并没有出现关于规格与代码部分的BUG。
五、 基本思路和体会
1、仔细阅读指导书，因为与指导书规定不符合被报BUG是最亏的
2、注意写jsf时统一一个规范，这样在与别人合作的时候，也可以更好的对接，使用布尔表达式不会导致二义性
3、时刻注意指导书的变化动态