BUAA_OO_Unit3_Summary

Posted 2021-02-18 yixuanluo

tags:

篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了BUAA_OO_Unit3_Summary相关的知识，希望对你有一定的参考价值。

一.JML语言理论基础与应用工具链

1.JML简介

　　JML(Java Mudeling Language)是一种语言行为规范，通过规范化的语句描述，约束了模块的行为。JML既可以用于规格化设计，又

　　可以用于针对已有代码的JML规格书写，提高代码的可读性与可维护性。

　　JML能够便于开发人员之间的交流，同时也能提高程序开发的效率与可维护性。总的来说，JML是对模块行为的精确化描述，有助

　　于我们有效地发现和改正错误。

　　2.JML语法

　　原子表达式：

　　　　1.esult: 表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。

　　　　2.old(expr): 表示一个表达式expr在相应方法执行前的取值，该表达式涉及到评估expr中的对象是否发生变化。需要注意的

　　　　是，当expr为引用类型时，修改被引用的内容不会导致expr产生变化，因为expr指向的地址没有变，产生变化的是该地址中的内容。

　　　　3.not_assigned(x,y,...): 用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true ，否则返回

　　　　false 。用于后置条件的约束，限制一个方法的实现不能对列表中的变量进行赋值。

　　量化表达式：

　　　　1.forall: 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。　　

　　　　 2.exists: 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。

　　　　 3.sum: 返回给定范围内的表达式的和。

　　　　 4.min: 返回给定范围内的表达式的最小值。　

　　　　 5.max: 返回给定范围内的表达式的最大值。

　　　方法规格

　　　 1.requires: 前置条件，要求调用者确保其后的条件为真

　　　　2.ensures：后置条件，对方法执行结果的限制。即在满足前置条件的情况下，保证执行结果满足后置条件，否则执行错误。

　　　　 3.assignable：副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。

　　　类型规格

　　　　invariant: 不变式，要求在所有可见状态下都必须满足的特性。

　　3.应用工具链

　　　Openjml : Openjml是用于检查与解析JML规范的工具，其本身并不对规格实现进行检查。不过它一般与SMT Solver(Z3、CVC4等)结

　　　合使用，它将解析出来的JML规范转换为SMT-LIB形式，并将Java程序本身的证明逻辑传给后端的SMT求解器。其解决问题的能力取

　　　其后端的SMT Solver。下载地址：http://www.openjml.org/

　　　　JUnit : JUnit是针对Java语言的单元测试框架。可以在其中对各个模块编写自己的单元测试代码，针对性地测试代码中的某一部分。

　　　　JMLUnitNg : 可以根据JML规格自动化生成测试用例，不过数据往往十分极端，参考价值不大。下载地址：

　　　http://insttech.secretninjaformalmethods.org/software/jmlunitng/

二.SMT Solver的部署

　　这里我们用到的SMT Solver是Z3。

　　Z3的安装和使用可以参考：https://www.cnblogs.com/zwqzj/p/10816245.html

　　public class Test {
　　　　public static void main(String[] args) {
        　　System.out.println(Test.div(10,5));
　　　　　　  System.out.println(Test.small(10,5));
    　　}

    　　//@ensures 
esult == a / b;
    　　public static int div(int a, int b) {
    　　    return a / b;
   　　 }
　　
　　　　 //@ensures 
esult == (sum char i; i >= ‘a‘ && i <= ‘z‘ && name.contains(i); 1)
   　　　public static int small(String name) {
　　　　　　　int sum = 0; 
       　　 for(char x : String name) {

　　　　　　　　  if (x <= ‘z‘ && x >= ‘a‘) {
　　　　　　　　　　　　sum++;
　　　　　　　　　}
　　　　　　　}
　　　　　　　return sum;
   　　 }
　　}

　　将Z3安装之Openjml对应目录下,并配置好相应的环境变量后，在命令行输入如下指令即可开始测试：

java -jar C:UsersDesktopopenjmlopenjml.jar -esc -prover cvc4 -exec C:UsersDesktopopenjmlSolvers-windowscvc4-1.6.exe C:UsersIdeaProjectsdemosrcTest.java

　　使用Openjml与Z3求解器对上述代码进行测试，得到两条INVALID报错，提示我们div无法处理b = 0的情况以及small在name = null的情况时无法得到正确结果。