OO第三次总结

1、规格化设计的发展历史

从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) 

 

2、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的全部问题，把天然语言的使用频率降到最低，并把逻辑表达式检查了一遍，并且认真添加了新代码，写了设计文档，可是。。。测试者并无给我测试。

 

3、规格bug产生缘由的分析

一开始是看课件和Guideline看的不够认真，没有理解其精髓，并且时间紧迫，因而就大面积使用天然语言，并且逻辑写得不够仔细。以后对JSF进行了全面修改，可是由于少改了一个类的JSF而又被报了bug。最后一次做业我把JSF所有检查了一遍，虽然此次做业测试者没有给我测试，可是我以为即便他测试了那也很难再挑出JSF的bug了。

 

4、规格的很差写法与改进

 一、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();
 @ */

二、忽略了必要的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;
 @ */

 

三、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;
 @ */

四、没有归纳异常状况

/**@ 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);
 @ */

五、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;
 @ */

 

5、功能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在方法上的汇集关系。

 

6、设计规格和撰写规格的基本思路和体会

一、基本思路

设计规格的时候要保证写得尽可能简洁，作到每一个方法只作一件事，这样在才能保证不会写出几百行长的超级方法，可是个人代码中仍然存在几百行长的超级方法，例如Driver类的run方法，由于当时写的时候没有要求规格，因此写得洋洋洒洒，后来也很差改了。写规格的时候要避免使用天然语言，例如队列的相关操做能够用contains和size等语言描述其EFFECTS。

二、体会

必定要先设计规格再写代码，训练本身设计规格和按照规格写代码的能力，先设计规格再写代码还能使代码写得更漂亮。