BUAAOO Unit3 形式化规格约束下进行编程
作者:互联网
§3 形式化规格约束下进行编程
S1 JML相关梳理
P0 作用
1)描述方法的功能,参数要求和输出结果,异常和正常行为
2)结合JML检查工具可以检测代码是否实现了预期功能,或者自动生成测试样例
P1 语法
0)注释格式:
//@ single line
/*@
@ block
@*/
1)行为:
- normal_behavior:正常行为
- exceptional_behavior:异常行为
- signals语句:
signals(E e) R
,当条件R满足时要求抛出异常E
- signals语句:
- 行为发生条件间不应当有交集
2)作用域
- public:只能用于public方法/字段
- private
- package
- protect
- spec_public:用于使一个private变量能够在规格中使用
3)前置条件和后置条件
- requires:前置条件,调用方法前应当满足的条件,通常限制参数
- ensures:后置条件,方法返回时应当满足的条件,通常限制返回值
4)模型域:JML注释的成员变量 model instance
//@ public model instance JMLObjectBag elementsInQueue
//@ public model static JMLObjectBag elementsInQueue
- 模型域到实现域的映射描述:
represent
5)副作用:方法执行后修改了字段的值
assignable
直接修饰的arg,或是arg依赖的变量,允许在方法执行中赋值modifiable
允许修改- 局部变量和方法形参也允许修改
- 形参代表的引用可以重新指向,但是不允许修改指向对象的值
- arg在方法开始时尚未分配,允许分配
- assign /noting 相当于 pure。assign /everything 表示方法可以修改任何变量
6)类级不变量:进入和退出一个类中每个方法都必须满足的条件
-
invariant
:不变量条件constraint
:变化约束条件,作用类似invariant,限制前后状态关系 -
分静态与非静态成员的约束:
//@ public instance invariant //@ public static invariant
7)布尔表达:
- 量词:
\forall
\exists
\min
- 关系: 蕴含
==>
<==
<=>
8)E<:E2
E1是E2 子类/同类
9)集合:new ST {T x| R(x) && P()}
P2 JML关键字与库函数
\result
返回值
\old(args)
返回调用前args
值
\not_assigned(args)
参数是否在方法执行过程中赋值
\not_modifed(args)
参数在方法执行期间取值不变
\nonnullelements(containner)
表示continner
中存储对象非null
\type(type)
返回type
对应的类Class
\typeof(expr)
返回expr
的准确类型
\sum
product
给定范围内表达式求和 积
//@ (\sum int i; 0 <= i && i < 5; i)
\max
\min
最大\小值
//@ (\max int i; 0 <= i && i < 5; i)
\num_of
满足条件的取值个数
//@ \num_of int x; R(x); P(x)
//equals to:
//@ \sum int x; R(x) && P(x); 1
P3 规格的继承
1)重载方法的规格需要使用 //@also 注释
2)为保证LSP原则,子规格应当满足一定约束:
- 子规格不变量蕴含父规格不变量
- 子规格副作用小于父规格副作用
- 子规格前后置条件蕴含父规格前后置条件
P4 JML相关工具链
1)OpenJML: 开源的JML工具,具有检查JML文档规格语法,逻辑问题的功能。早期我用它进行过JML文档语法的静态测试。
2)JMLUnitNG:基于JML的单元测试工具,支持自动生成测试样例
3)JMLEclipse:Eclipse自带的JML插件
注:关于JML工具链的尝试:
-
OpenJML:许久前用其测过JML文档语法。由于自带说明书,用起来还是比较方便。如果要动态测试,需要编写represent实现模型域到实现域的映射。
-
JMLUnitNG:写了简单的测试程序
public class Test{ /*@ public normal_behavior @ ensures \result == a+b @*/ public static int add(int a, int b) { return a+b; } }
运行结果:
JMLUnit主动测试了边界范围的值,并没有做一般性测试。
-
Group的测试。一如既往,JMLUnitNG只会测试边界,由于它不会生成Person,所以它总是丢个null进去
S2 作业分析
1)架构分析:本次作业的规格都已由课程组给出。经过Metric量化分析,发现结构非常合理。
2)算法分析:
- 在isCircle中使用了并查集算法,在每次加入新成员时,分配一个新的连通块。当加入联系时,若联系的两个人处于不同连通块,则合并这两个连通块。在合并操作中,我选择修改包含成员数少的连通块中成员的连通块号。据了解有另一种做法是维护一个AVL,但是这样做在查找某位成员的连通块号的时候需要进行遍历。经过考虑,我选择了前者。理由是这种实现更快,而且我认为连通块查询频率高于修改频率,这样做更加符合实际。
- 在queryStrongLink中使用了Tarjan的魔改算法,没有记录所有的点双连通块,仅仅记录根节点(id1)所在的点双连通块,查找其中有无出现过(id2)并且块大小大于2。这样做减少了空间和时间开销。同时不同于常见的点双连通算法将边入栈的做法,我将点入栈,并且在查找到割点时,不将割点退栈。这样实现更快,也不需要添加多余的边类。
- 在queryMinPath中使用了堆优化DIJ算法。使用了内置的PriorityQueue优先队列,因此实现也很快。
- 对于Group,使用了效率从属变量方式,保存待查询的变量。这样修改其值很方便。缺点是relationsum这一属性与network是耦合的。
3)测试分析:
- 第一次作业中,我由于将p.queryValue(q)=0等价于!p.islink(q),导致错了三个点。主要是测试不足
- 后两次作业中,由于采取充分测试,没有出bug。
- 测试中结合黑白盒测试。Junit负责测试边界情况。黑盒测试进行压力测试和一般情况测试,并尝试找出白盒测试中的盲点。
S3 心得体会
1)在本单元中,我才初步开始进行测试。在测试中我了解到,白盒测试往往用于功能性检查,黑盒测试往往用于鲁棒性检查。在白盒测试中总是很难做到全面的测试覆盖。
2)对于规格语言的理解:规格语言形式化地描述了程序的行为。我认为规格语言主要在开发之前作为思路梳理,避免后续编程中过于投入而失去整体把握。规格语言有利于产品经理与程序员沟通。同时,也明确定义了需求。但是我觉得JML实际上是为方法编写了一个等价实现。规格不一定要使用JML来描述,我觉得使用Python这样浅显易懂的语言来编写规格文档也可以起到相同的效果。其次,JML工具链并不成熟,许多测试工具没能正常运行。测试工具对于exisit array这样的规格描述基本无能为力。
标签:连通,JML,int,形式化,规格,BUAAOO,测试,Unit3,public 来源: https://www.cnblogs.com/TwoBeNo-0/p/12920470.html