OO第三单元——JML

Posted 2021-02-18 aaaa2020

OO第三单元总结——JML

一、梳理JML语言的理论基础、应用工具链情况

JML语言理论基础

JML是一种形式化的、面向JAVA的行为接口规格语言（Behavior Interface Speci?cation Language，BISL），基于Larch方法构建 。BISL提供了对方法和类型的规格定义手段。

JML的两种主要用法：

• 开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。

• 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

1.注释结构

JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。

• 前置条件(pre-condition)：定义了过程对输入的约束要求。

• 副作用范围限定(side-e?ects)：过程在执行过程中对Input的修改。

• 后置条件(post-condition)：定义了过程在所有未被requires排除的输入下给出的执行效果。

2.JML表达式

• 原子表达式

  • esult表达式：表示一个非void 类型的方法执行所获得的结果。
  • old( expr )表达式：用来表示一个表达式expr 在相应方法执行前的取值。
  • ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
  • ot_modified(x,y,...)表达式：与上面的 ot_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
  • onnullelements( container )表达式：表示container 对象中存储的对象不会有null。
  • ype(type)表达式：返回类型type对应的类型(Class)。
  • ypeof(expr)表达式：该表达式返回expr对应的准确类型。

• 量化表达式

  • forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
  • exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
  • sum表达式：返回给定范围内的表达式的和。
  • product表达式：返回给定范围内的表达式的连乘结果。
  • max表达式：返回给定范围内的表达式的最大值。
  • min表达式：返回给定范围内的表达式的最小值。
  • um_of表达式：返回指定变量中满足相应条件的取值个数。

• 集合表达式

  • 集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。

• 操作符

  • 子类型关系操作符： E1<:E2 ，判断类型E1是否为类型E2的子类型(sub type)。
  • 等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 。
  • 推理操作符： b_expr1==>b_expr2 或者b_expr2<==b_expr1 。
  • 变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。 othing指示一个空集；everything指示一个全集，即包括当前作用域下能够访问到的所有变量。

3.方法规格

• 前置条件通过requires子句来表示： requires P;。

• 后置条件通过ensures子句来表示： ensures P;。

• 副作用范围限定：使用关键词 assignable 或者 modifiable 。

• signals子句：signals子句的结构为 signals (***Exception e) b_expr;。还有一个简化的signals子句，即signals_only子句，后面跟着一个异常类型。

• public normal_behavior ：方法的正常功能。

• public exceptional_behavior ：方法的异常功能。

• 关键词 also

4.类型规格

• 不变式invariant :不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义invariant P ，其中invariant 为关键词， P 为谓词。

• 状态变化约束constraint：对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。JML为了简化使用规则，规定invariant只针对可见状态(即当下可见状态)的取值进行约束，而是用constraint来对前序可见状态和当前可见状态的关系进行约束。

应用工具链

• openjml：内置SMT Solver, 以静态方式检查代码实现对规格的满足程度。

• JMLUnit/JMLUnitNG：针对JML自动生成测试用例。

二、部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果

参考https://www.cnblogs.com/lutingwang/p/openjml_basic.html，使用openjml。

1.语法检查

//Person.java 代码段
//@ ensures 
esult.equals(name)
public /*@pure@*/ String getName();

//@ ensures 
esult.equals(character);
public /*@pure@*/ BigInteger getCharacter();

//@ ensures 
esult == age
public /*@pure@*/ int getAge();

报错：

2.静态检查

public class Test {
	/*@
	  @ requires  a <1111;
	  @ ensures 
esult == a+1;
	  @*/
	public static int add(int a) {
		return a+1;
	}
	public static void main(String[] args) {
		add(1111);
	}
}

报错：

3.动态检查

参考的方法运行不了，换了一种方式，在openjml文件夹中输入java -cp jmlruntimr.jar; Test

public class Test {
	/*@
	  @ requires  a <1111;
	  @ ensures 
esult == a+1;
	  @*/
	public static int add(int a) {
		return a+1;
	}
	public static void main(String[] args) {
		add(1111);
	}
}

报错：

三、部署JMLUnitNG/JMLUnit，针对Group接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析

先下载JMLUnitNG：http://insttech.secretninjaformalmethods.org/software/jmlunitng/
点击1.4即可下载。

使用步骤如下：

• java -jar jmlunitng.jar MyGroup.java
• javac -cp jmlunitng.jar *.java
• java -cp jmlunitng.jar MyGroup_JML_Test

生成测试文件：

运行测试文件：

可以看出，生成的测试用例都是一些比较极端的数据，如：空指针null、INT_MAX、INT_MIN、0等。这样测试不具有全面性，覆盖率低。

四、按照作业梳理自己的架构设计，特别分析自己的模型构建策略

1.第九次作业

• 架构设计

  比较复杂的方法是isCircle，采用dfs实现，为了更好的存储已经访问过的点，给每个Person增加了一个属性pos，记录位置。而且因为Network不会删除Person，所以实现起来较为简便。其他按规格中的层次来设计实现。

• 模型构建策略

  采用HashMap和ArrayList同时存储数据，因为Person的id是唯一的，ArrayList用来遍历，HashMap用来查找，以空间换时间。Person就相当于点，且存储了与之相连接的点，而Network就是包含Person的图。

2.第十次作业

• 架构设计

  增加了Group接口，实现了MyGroup类。由于数据很大，所以对于Group求平均数、方差以及relationSum等数，选择在Group中addPerson时计算增加ageSum、relationSum等值。然后query的时候，直接返回，而不需要遍历计算。有可能爆栈，isCircle实现将dfs改为bfs。

• 模型构建策略

  沿用第九次作业的策略，采用HashMap和ArrayList同时存储数据。

3.第十一次作业

• 架构设计

  这次作业在Network中增加了许多查询方法，其中比较影响性能的有queryMinPath（查找两个人之间的最小路径及最小valueSum）、queryStrongLinked（询问两个人是否为强连接即是否有环包含这个两个人且环中至少有三个人）、queryBlockSum（Network中有几个块/集合）。

  queryBlockSum中查找有几个块，可以使用dfs/bfs/并查集实现，因为并查集可以缓存每个Person的根节点，所以queryBlockSum和isCircle都采用并查集实现。

  queryMinPath采用Dijkstra+堆优化实现。

  queryStrongLinked采用tarjan实现。

  Group中增加delPerson方法，实现和addPerson类似。

• 模型构建策略

  沿用第十次作业的策略，采用HashMap和ArrayList同时存储数据。模型没有很大变化，主要是Network中增加了许多图查询。其中queryMinPath中涉及distance，为了使操作简便，在Person中增加了dst属性，而不是使用数组。

五、按照作业分析代码实现的bug和修复情况

1.第九次作业

bug就是isCircle方法的JML理解错误，以为要按add加入顺序看是否联系得到，我也很奇怪当时为什么会这么想，可能是array[i+1]给了我错觉。重新写了dfs修复了bug。

2.第十次作业

无bug。

3.第十一次作业

无bug。

六、阐述对规格撰写和理解上的心得体会

虽然第九次作业看起来十分的简单，但还是翻车了，连互测都没进，只能说大意失荆州。但是第九次作业的失误，让我对第十次作业和第十一次作业更加认真和仔细。认真分析如何实现代码，数据怎么存储，才能在满足规格的情况下，获得更好的性能。也会更加认真地做测试，发现了几个bug。

由于这单元地重点是根据规格写代码，所以题目在图论方面出的不是特别难，数据也没有特别刁钻。总体而言还是比较简单的。虽然只需要实现规格，但是根据数据我们还要考虑性能，这也比较符合实际情况。而且我们也不能完全照着规格写，因为规格其实相当于注释，只是告诉你要做什么，具体实现还是要仔细思考，适当做出调整。