第三次博客

一、 规格发展历史

从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统计及分析

分析：

自己使用的自然语言太多，就不能很好的满足条件，而且，有些规格以为可以不写，就没写，比如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:\result==>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:
　　　　@ */

四、 聚焦关系

基本没有什么关系。

五、 思路体会

以后要更深入地理解规格，不用自然语言，为了提高代码质量而写规格，为了提升自己而去学习，让自己在这些方面变得完美。

原文地址：https://www.cnblogs.com/Arsenalgooner/p/9107560.html