标签：val 返回值 sync tomat 交流 AC 风格 jks 用户
一、规格化设计的发展历史以及为什么得到重视
规格的历史：
从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
为什么得到人们重视：
程序的设计要求具有明确的逻辑，而自然语言具有二义性，这就使得前人的程序无论是被用户拿到还是被维修者拿到都难以很好利用。如果拥有一种统一的，意义明确的语言，那么对开源程序的发展是非常有利的。这就是规格化设计受到重视的原因
此外，规格化设计对于开发者本身而言也具有重大的意义，一方面，可以使开发者明确自己要做什么，自己的程序中每个部分都起到了哪些作用，有助于完善代码中其他部分。另一方面，开发者自己时间长了也有可能忘记曾经的设计思路以及方法的行为，这时规格可以有效唤醒开发者的记忆。
二、规格bug
本人在这几次作业中，并没有被测试者提出规格上的bug。但是，本人自己认为在程序规格中，存在着一些问题，在后文中会加以说明。
三、规格产生原因
对于规格的理解不深，在规格的撰写中，存在着敷衍的态度问题，并没有体会到规格的好处，也就对良好的规格撰写缺乏动力和印象。
四、不足与改进
A、前置
1、使用多余的前置条件
前：@REQUIRES: !tlist.isEmpty && m.isvalid;
后：@REQUIRES: !tlist.isEmpty;
实际上无效的请求根本不会加入到请求列表中，而且该类及方法的执行不应对请求的内容予以辨认，这是外界传入方法的责任。对于无效请求的处理应当在代码中实现。
2、忽略应当要求的范围限制
方法：public synchronized static ArrayList<Point> flashback(point E,point S)
前：@REQUIRES: E!=null && S!=null;
后：@REQUIRES: 0<= E.getx() <=79&&0<= E.gety() <=79 && 0<= S.getx() <=79&&0<= S.gety() <=79
3、使用伪布尔表达式
前：@REQUIRES: taxi!=null;
后：@REQUIRES: taxi instance of singleTaxi && taxi!=null;
4、缺乏类型描述
前：@REQUIRES: file.exists&&map!=null&&taxi!=null&&guest!=null;
后：@REQUIRES: file.exists == true&&map!=null&&taxi!=null&&guest!=null;
5、大量使用None
方法：public int fromto(Point here, Point there)
前：@REQUIRES: None;
后：@REQUIRES: 0<= here.getx() <=79&&0<= here.gety() <=79 && 0<= there.getx() <=79&&0<= there.gety() <=79;
B、后置
1、使用伪布尔表达式
前：@EFFECTS : mapmap.contains(File(map).toMatrix);
后：@EFFECTS : mapmap.contains(File(map).toMatrix) == true;
2、限制不够明确
前：@EFFECTS : (\all singleTaxi e;tlist.contains(e);e.state ==2 && e.exist(m.fromx,m.fromy)) ==> thislist.contains(e)
后：@EFFECTS : ((\all singleTaxi e;tlist.contains(e);e.state ==2 && this.x-2<=m.fromx<=this.x+2 && this.y-2<=m.fromy<=this.y+2) ==> thislist.contains(e)
尽量使用明确的数值之间的关系，而不是使用抽象的方法，甚至使用不存在的方法——其实也就是自然语言糊弄过去。
3、不能明确\old应当使用的场合
前：@EFFECTS : this.x == this.x + 1；
后：@EFFECTS : this.x == (\old)this.x + 1;
4、忘记多方面考虑EFFECTS
前：@EFFECTS：list.contains(e) == true;
后：@EFFECTS：list.contains(e) == true && list.size() == (\old)list.size() + 1;
5、不应使用自然语言描述
前：@EFFECTS : tlist.contains(\all \within limitation singleTaxi)；
后：@EFFECTS : (\all singleTaxi e;tlist.contains(e);e.state ==2 && e.exist(m.fromx,m.fromy)) ==> thislist.contains(e) == true;
五、聚焦关系
本人在规格上未被报BUG，所以聚焦关系在表面上是不存在的。
实际上，本人的程序BUG全都是设计完成度和准确性的缺少，和规格上可能存在的问题缺乏交集。
唯一的一处可以举出：我错误的理解了指导书，导致一个判断条件写错了，错误地删除了接单出租车列表中的部分出租车，如果我能够检查在规格中指出的清空的条件和结果，也许会更快发现这个问题。
方法名：Monitor线程中的Run()
功能BUG数：1
规格BUG数：1
六、思路与体会
心得体会：
①REQUIRES、MODIFIES、EFFECTS的撰写必须考虑周全，不要多加，更不能缺失。对于REQUIRES需要从反面考虑哪些情况会导致方法出错，对于MODIFIES需要从用户和外界角度上考虑，对于EFFECTS需要考虑返回值以外的情况。
②前置后置条件均应尽量使用布尔表达式，需要减少二义性的描述。对于前置条件，应上升到禁止的层次
③不要敷衍地写一些诸如None，xx.contains(aa)之类的不负责任的规格
④规格对方法应起到宪法对法律的作用，但又不能太粗略
个人感受：
规格最好是在方法开始撰写之前便开始设计，在之后的代码设计中也要尽量按照写出的规格来完成。如果发现在规格设计上存在缺陷，或是代码设计不能满足规格设计的要求，那么应当边调整边完善代码，而不是在方法完成以后，再去撰写规格。
这几次的规格撰写说实话是失败的，就本人个人和同学之间的交流而言，JSF、Overview、RepOK等要求带给我们的只有打补丁一样的厌烦感，而不是整齐的风格和清晰的逻辑。希望以后的工作学习中能够进行一次系统的程序设计。
标签：val 返回值 sync tomat 交流 AC 风格 jks 用户
原文地址：https://www.cnblogs.com/zhc16061015/p/9108684.html
