标签：副作用 面具 删除 normal 法规 static 缓存 返回 部署
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表达式
原子表达式
量化表达式
集合表达式
操作符
E1<:E2 ，判断类型E1是否为类型E2的子类型(sub type)。b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 。b_expr1==>b_expr2 或者b_expr2<==b_expr1 。\nothing指示一个空集；\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自动生成测试用例。
参考https://www.cnblogs.com/lutingwang/p/openjml_basic.html，使用openjml。
1.语法检查
//Person.java 代码段
//@ ensures \result.equals(name)
public /*@pure@*/ String getName();
//@ ensures \result.equals(character);
public /*@pure@*/ BigInteger getCharacter();
//@ ensures \result == age
public /*@pure@*/ int getAge();
报错：
2.静态检查
public class Test {
/*@
@ requires a <1111;
@ ensures \result == 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 \result == a+1;
@*/
public static int add(int a) {
return a+1;
}
public static void main(String[] args) {
add(1111);
}
}
报错：
先下载JMLUnitNG：http://insttech.secretninjaformalmethods.org/software/jmlunitng/
点击1.4即可下载。
使用步骤如下：
生成测试文件：
运行测试文件：
可以看出，生成的测试用例都是一些比较极端的数据，如：空指针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属性，而不是使用数组。
1.第九次作业
bug就是isCircle方法的JML理解错误，以为要按add加入顺序看是否联系得到，我也很奇怪当时为什么会这么想，可能是array[i+1]给了我错觉。重新写了dfs修复了bug。
2.第十次作业
无bug。
3.第十一次作业
无bug。
虽然第九次作业看起来十分的简单，但还是翻车了，连互测都没进，只能说大意失荆州。但是第九次作业的失误，让我对第十次作业和第十一次作业更加认真和仔细。认真分析如何实现代码，数据怎么存储，才能在满足规格的情况下，获得更好的性能。也会更加认真地做测试，发现了几个bug。
由于这单元地重点是根据规格写代码，所以题目在图论方面出的不是特别难，数据也没有特别刁钻。总体而言还是比较简单的。虽然只需要实现规格，但是根据数据我们还要考虑性能，这也比较符合实际情况。而且我们也不能完全照着规格写，因为规格其实相当于注释，只是告诉你要做什么，具体实现还是要仔细思考，适当做出调整。
标签：副作用 面具 删除 normal 法规 static 缓存 返回 部署
原文地址：https://www.cnblogs.com/aaaa2020/p/12943679.html
