第三次博客
一、 规格发展历史
从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次作业 |
11 |
0 |
否 |
|
第10次作业 |
10 |
2 |
否 |
|
第11次作业 |
6 |
3 |
否 |
分析：
自己使用的自然语言太多，就不能很好的满足条件，而且，有些规格以为可以不写，就没写，比如repok。
三、 规格举例
１、使用自然语言
/** @REQUIRES: r!=null
*@MODIFIES: this
*@EFFECTS: 给this里的变量赋值
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
修改后：
/** @REQUIRES: r!=null
*@MODIFIES: this
*@EFFECTS: this!=null
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
2、前置条件必须为布尔表达式
/** @REQUIRES: r范围为0-300
*@MODIFIES: this
*@EFFECTS: this!=null
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
修改后：
/** @REQUIRES: 0<=r<300
*@MODIFIES: this
*@EFFECTS: this!=null
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
3、忽略了effects
/**@REQUIRES:
*@MODIFIES:
*@EFFECTS:None
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
改进后:
/**@REQUIRES:
*@MODIFIES:
*@EFFECTS:
esult==>value
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/
4、effect直接使用代码。
/** @ REQUIRES: r!=null
@ MODIFIES: this
@ EFFECTS: r=r+1
@ THREAD_REQUIRES:
@ THREAD_EFFECTS:
@ */
改进后:
/** @ REQUIRES: r!==null
@ MODIFIES: this
@ EFFECTS: r==old(r)+1
@ THREAD_REQUIRES:
@ THREAD_EFFECTS:
@ */
四、 聚焦关系
基本没有什么关系。
五、 思路体会
以后要更深入地理解规格，不用自然语言，为了提高代码质量而写规格，为了提升自己而去学习，让自己在这些方面变得完美。