标签：总结 info cts rac lan temp lun 角度 file
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。通过JML及其支持工具，不 仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满 足情况。
通过参考 JML Level 0手册 ，组成内容如下：
（1）注释结构：
（2）JML表达式：
（3）方法规格：
（4）类型规格：
类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计 的约束规则。
SMT，全称Satisfiability modulo theories，是验证一阶逻辑具有相等性逻辑公式的决策问题。而这里我们可以用SMT Solver来验证我们实现的程序和JML规格的功能是否等价。
z3 solver是Microsoft Research开发的一种较为高效的SMT Solver库，同时又由于openJML本身支持z3 solver进行验证，所以我这里直接采用openJML自带的z3 solver程序进行验证。
在使用openJML确定自己的jml规格没有语法错误后（具体方法在下一部分），可通过如下指令使用openJML和附带的z3 solver验证自己实现的代码。
java -jar openjml\openjml.jar -exec openjml\Solvers-windows\z3-4.7.1.exe -esc test\MyGroup.java test\Person.java
如果验证结果正确，应得到如下结果。（那个警告大家无视就好，这个主要是因为solver不让初始化为null）
通过添加参数 -verboseness=3 后，我们可以得到验证过程的全部输出： output.rar 。
我们可以从这个文件中看到z3 solver对MyGroup类的全部方法的验证过程，但是由于验证过程输出过长，这里只展示三个主要方法的部分验证过程。
构造方法MyGroup()
TRANSFORMATION OF test.MyGroup.MyGroup(int)
{
java.lang.Exception `exception = null;
int `terminationPosition = 0;
int __JML_AssumeCheck_;
// Declaration of THIS
test.MyGroup `THIS;
/*@ assume `THIS != null;*/
/*@ assume `THIS == null || `THIS instanceof test.MyGroup && (\typeof(`THIS) == \type(test.MyGroup) && <:(\typeof(`THIS), \type(test.MyGroup)));*/
/*@ assume `THIS.`alloc__ == 1;*/
// Declare formals
int id1;
// Declare result of constructor
test.MyGroup `result = `THIS;
// Heap value and allocation fields
{
// Invariants for discovered fields
/*missing*/
/*missing*/
/*missing*/
}
// Assume axioms
// axiom (\forall \bigint m, \bigint n; m > n && n >= 0; pow256(m) > pow256(n));
addPerson()
TRANSFORMATION OF test.MyGroup.addPerson(test.Person)
{
java.lang.Exception `exception = null;
int `terminationPosition = 0;
int __JML_AssumeCheck_;
// Declaration of THIS
test.MyGroup `THIS;
/*@ assume `THIS != null;*/
/*@ assume `THIS == null || `THIS instanceof test.MyGroup && <:(\typeof(`THIS), \type(test.MyGroup));*/
/*@ assume `THIS.`alloc__ == 0;*/
// Declare formals
/*@ non_null */
test.Person person;
// Heap value and allocation fields
{
// Invariants for discovered fields
/*missing*/
/*missing*/
/*missing*/
{
/*@ assume key != null;*/
/*@ assume (key == null || key instanceof java.lang.Object && <:(\typeof(key), \type(java.lang.Object))) && (key == null || key instanceof java.lang.Comparable && <:(\typeof(key), \type(java.lang.Comparable))) && (key == null || key instanceof java.io.Serializable && <:(\typeof(key), \type(java.io.Serializable))) && (key == null || key instanceof java.lang.Number && <:(\typeof(key), \type(java.lang.Number))) && (key == null || key instanceof java.lang.Integer && <:(\typeof(key), \type(java.lang.Integer)));*/
// assume ImplicitAssume (key == null || key instanceof java.lang.Object && <:(\typeof(key), \type(java.lang.Object))) && (key == null || key instanceof java.lang.Comparable && <:(\typeof(key), \type(java.lang.Comparable))) && (key == null || key instanceof java.io.Serializable && <:(\typeof(key), \type(java.io.Serializable))) && (key == null || key instanceof java.lang.Number && <:(\typeof(key), \type(java.lang.Number))) && (key == null || key instanceof java.lang.Integer && <:(\typeof(key), \type(java.lang.Integer))); ...
}
hasPerson()
TRANSFORMATION OF test.MyGroup.hasPerson(test.Person)
{
java.lang.Exception `exception = null;
int `terminationPosition = 0;
int __JML_AssumeCheck_;
// Declaration of THIS
test.MyGroup `THIS;
/*@ assume `THIS != null;*/
/*@ assume `THIS == null || `THIS instanceof test.MyGroup && (\typeof(`THIS) == \type(test.MyGroup) && <:(\typeof(`THIS), \type(test.MyGroup)));*/
/*@ assume `THIS.`alloc__ == 1;*/
// Declare formals
int id1;
// Declare result of constructor
test.MyGroup `result = `THIS;
// Heap value and allocation fields
{
// Invariants for discovered fields
/*missing*/
/*missing*/
/*missing*/
}
{
/*@ assume temPerson != null;*/
/*@ assume (temPerson == null || temPerson instanceof java.lang.Object && <:(\typeof(temPerson), \type(java.lang.Object))) && (temPerson == null || temPerson instanceof test.Person && <:(\typeof(temPerson), \type(test.Person)));*/
// assume ImplicitAssume (temPerson == null || temPerson instanceof java.lang.Object && <:(\typeof(temPerson), \type(java.lang.Object))) && (temPerson == null || temPerson instanceof test.Person && <:(\typeof(temPerson), \type(test.Person))); ...
}
{
/*@ assume -2147483648 <= singleVar && singleVar <= 2147483647;*/
// assume ImplicitAssume -2147483648 <= singleVar && singleVar <= 2147483647;
}
以上这三个函数的验证过程其实还有很多，但实在限于篇幅，所以只能截取部分。但是我们可以从中看到一些共性的验证内容：
注意在使用JMLUnitNG进行测试前，首先需要使用openJML检测程序的JML语法是否正确。
对于openJML，个人认为目前较为简便的使用方式是通过命令行，其他比如使用IDEA的External tools或者eclipse的插件的使用方式，本人在使用的过程中产生了各种奇奇怪怪的问题，并且很难解决。
通过openJML检查MyGroup类的jml语法并且修改jml错误后，本人最终得到完全正确的MyGroup类JML如下：
import java.math.BigInteger;
import java.util.HashMap;
public class MyGroup {
/*@ public instance model non_null int id;
@ public instance model non_null Person[] people;
@ public instance model non_null int relationSum;
@ public instance model non_null int valueSum;
@*/
private int id1;
private HashMap<Integer,Person> people1;
public MyGroup(int id1) {
this.id1 = id1;
people1 = new HashMap<Integer, Person>();
}
//@ ensures \result == id;
public /*@ pure @*/ int getId() {
}
/*@ also
@ public normal_behavior
@ requires obj != null && obj instanceof MyGroup;
@ assignable \nothing;
@ ensures \result == (((MyGroup) obj).getId() == id);
@ also
@ public normal_behavior
@ requires obj == null || !(obj instanceof MyGroup);
@ assignable \nothing;
@ ensures \result == false;
@*/
public boolean equals(Object obj) {
}
/*@ public normal_behavior
@ assignable people;
@ ensures people.length == \old(people.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(people.length);
@ (\exists int j; 0 <= j && j < people.length;
@ people[j] == \old(people[i])));
@ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person);
@*/
public void addPerson(Person person) {
}
//@ ensures \result == (\exists int i; 0 <= i && i < people.length; people[i].equals(person));
public boolean hasPerson(Person person) {
}
/*@ ensures \result == (\sum int i; 0 <= i && i < people.length;
@ (\sum int j; 0 <= j && j < people.length && people[i].isLinked(people[j]); 1));
@*/
public int getRelationSum() {
}
/*@ ensures \result == (\sum int i; 0 <= i && i < people.length;
@ (\sum int j; 0 <= j && j < people.length &&
@ people[i].isLinked(people[j]); people[i].queryValue(people[j])));
@*/
public int getValueSum() {
}
/*@ public normal_behavior
@ requires people.length > 0;
@ ensures (\exists BigInteger[] temp;
@ temp.length == people.length && temp[0] == people[0].getCharacter();
@ (\forall int i; 1 <= i && i < temp.length;
@ temp[i] == temp[i-1].xor(people[i].getCharacter())) &&
@ \result == temp[temp.length - 1]);
@ also
@ public normal_behavior
@ requires people.length == 0;
@ ensures \result == BigInteger.ZERO;
@*/
public BigInteger getConflictSum() {
}
/*@ public normal_behavior
@ requires people.length == 0;
@ ensures \result == 0;
@ also
@ public normal_behavior
@ requires people.length != 0;
@ ensures \result == ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length);
@*/
public /*@ pure @*/ int getAgeMean() {
}
/*@ public normal_behavior
@ requires people.length == 0;
@ ensures \result == 0;
@ also
@ public normal_behavior
@ requires people.length != 0;
@ ensures \result == ((\sum int i; 0 <= i && i < people.length;
@ (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) /
@ people.length);
@*/
public int getAgeVar() {
}
/*@ public normal_behavior
@ assignable people;
@ ensures people.length == \old(people.length) - 1;
@ ensures (\forall int i; 0 <= i && i < people.length;
@ (\exists int j; 0 <= j && j < \old(people.length);
@ people[i] == \old(people[j])));
@ ensures (\exists int i; 0 <= i && i < \old(people.length); \old(people[i]) == person);
@*/
public void delPerson(Person person) {
}
/*@ public normal_behavior
@ assignable relationSum, valueSum;
@ ensures relationSum == \old(relationSum) + 2;
@ ensures valueSum == \old(valueSum) + 2 * value;
@*/
public void update(int value) {
}
//@ ensures \result == people.length;
public int getPeopleSum() {
}
}
要对此JML代码使用openJML检查语法，则执行指令：
java -jar openjml\openjml.jar -check -dir test\MyGroup.java test\Person.java
若得到下图结果，则说明语法正确。
若语法存在任何问题，将得到类似下图的结果。
而本人在使用openJML的过程中，还遇到了以下几类比较棘手的问题，想在这里给大家分享一下：
由于之前已经使用openJML检查过Group类的JML语法，所以接下来如果想使用JMLUnitNG进行测试，需要修改的部分就简单了许多，只需注意如下问题需要修改。
接下来分别执行以下三条指令来运行JMLUnitNG进行测试
java -jar jmlunitng.jar jmlunitngTest\MyGroup.java
javac -cp jmlunitng.jar jmlunitngTest\*.java
java -cp jmlunitng.jar jmlunitngTest.MyGroup_JML_Test
我这里分别解释一下每条指令的作用：
最终得到如下运行结果
测试分析
第一次作业
作业类图如下
架构设计
设计难点
第二次作业
作业类图如下
架构设计
设计难点
第三次作业
作业类图如下
架构设计
设计难点
模型构建策略：
本单元接触的规格化设计语言JML，让我对代码设计和代码实现之间的关系理解的更为透彻。进行规格化设计的工作者并不需要考虑方法的具体实现方式和内容，只需要通过JML规格撰写将方法的功能描述完整；进行代码实现的人员也只需要在读懂JML规格的需求后考虑如何实现，而不需要考虑设计层面的问题。这样就较为巧妙地实现了团队开发过程中地分工问题，提高了开发效率。同时，如果开发过程中出现bug，通过JML的相关工具链，也更容易定位错误出现的原因，也提高了解决bug的效率。
此外，虽然规格化设计并未对代码实现过程进行约束，但是其仍然具有较强的严谨性。相较于带有内在模糊性的自然语言描述，规格化设计逻辑严格，能够更加清楚的表达设计者内心的思想，也具有相应的验证方式。由此可见，在这一方面上，规格化设计具有较为严谨的优势。
总之，在本单元中，通过学习JML这个规格化设计语言，让我更加认识到了面向对象程序编写过程中代码设计这一操作的重要性。正是因为能够有严谨详细的规格设计，我们才能在程序编写和代码实现的过程中具有更高的效率。
标签：总结 info cts rac lan temp lun 角度 file
原文地址：https://www.cnblogs.com/OmedetoHe/p/12942373.html
