OO第三单元总结--根据JML写代码

时间 2020-05-10

标签第三单元总结根据 jml 代码繁體版

原文原文链接

一. JML语言

1. 理论基础

　　首先，JML不是JAVA的一部分，它是一群研究者为JAVA设计的扩展部分，但尚未获得官方的支持。所以，JAVA编译器并不支持JML，因此要想JML起做用，只能采用相似openJML这样的第三方来编译，将JML 规格编译为运行时检查的语句，即RAC code(runtime assertion checking)。若是代码实现与其JML规格不一致，将引起运行时JML exception。java

　　JML听从契约式设计范式(DBC)，Design by contract是软件开发的一种方法，核心是类与其客户之间达成契约。JML是一种形式化的、面向 JAVA的行为接口规格语言。node

　　推荐一篇step by step以一个比较复杂的例子来说解JML语法和设计的教程：https://www.ibm.com/developerworks/library/j-jml/git

2. 应用工具链

jmlrac: test for violations of assertions during execution
ESC/Java2: static verification; compile-time proving that contracts are never violated
jmldoc: javadoc-style documentation
jmlc: assertion-checking compiler
jml4c: a new JML compiler built upon the Eclipse JDT open-source platform

　　上述工具不少都已经再也不维护（跟不上java的升级，大多支持到java 1.5）, 看你们抱怨openJML坑，就想找找有没有更好用的JML工具，结果发现openJML居然是最好用的。架构

openJML：目前对JML支持最好，维护最积极的JML编译器了
jmlunit/jmlunitNG: unit testing tool

二. 部署SMT Solver

　　maven+openJML+Eclipse试了一下午仍是报错，命令行没试过，不知道怎么样，这一部分只好放弃了。maven

二. JMLUnitNG

　　下述过程可复现，代码和运行结果是一致的，若是有兴趣，能够参照个人步骤在本地试一试。函数

　　配置过程参见讨论区https://course.buaaoo.top/assignment/71/discussion/199 ，为了保证配置成功，我也是在Linux下配置。工具

　　Graph接口方法的规格几乎所有含有 \exists 或 \old，根本搞不了，因而只能退而求其次，去验证Path类。Path类里面的\sum等语法也不支持，因而我就模仿MyPath，写了个比减法稍复杂的demo。测试

 1 // yifan/MyPath.java
 2 package yifan;  3 
 4 public class MyPath {  5     private/*@ spec_public @*/ int[] nodes;  6 
 7     public MyPath(int[] nodeList) {  8         nodes = new int[nodeList.length];  9         for (int i = 0; i < nodeList.length; i++) { 10             nodes[i]=nodeList[i]; 11  } 12  } 13 
14     //@ ensures \result == nodes.length;
15     public /*@pure@*/ int size() { 16         return nodes.length; 17  } 18 
19     /*@ requires index >= 0 && index < size(); 20  @ assignable \nothing; 21  @ ensures \result == nodes[index]; 22  @*/
23     public /*@pure@*/ int getNode(int index) { 24         return nodes[index]; 25  } 26 
27     //@ ensures \result == (nodes.length >= 2);
28     public /*@pure@*/ boolean isValid() { 29         return nodes.length >= 2; 30  } 31 
32     public static void main(String args[]) { 33         return; 34  } 35 }

运行过程 step-by-step：ui

./jmlunitng yifan/MyPath.java javac -cp jmlunitng.jar yifan/**/*.java ./openjml -rac yifan/MyPath.java javac -cp jmlunitng.jar yifan/MyPath_InstanceStrategy.java java -cp jmlunitng.jar yifan.MyPath_JML_Test

运行前目录google

运行后目录

运行结果

结果讨论

MyPath(null)，MyPath.java中会调用length，错误，意料之中；
明明已经requires index>=0了，为何生成的测试例子里还会有负数？就算刚开始nodes=new int[10]，避免nodes为null的状况仍是这种结果；
彷佛JmlUnitNG只会生成int的边界值和0，无论requires? 这只是个人猜测。

有个问题须要讨论一下：

为何不写成

//@ public instance model non_null int[] nodes;
    private ArrayList<Integer> nodes;

openJML会把规格和实现里的nodes当成一个nodes，会报错。

那这么写不就好了吗？

//@ public instance model non_null int[] nodes;
    private ArrayList<Integer> myNodes;

非也，会报下述错误

yifan/MyPath.java:6: 警告: JML model field is not implemented: nodes
    //@ public model int[] nodes;
                           ^

nodes没实现？对的。要想解决这个问题，就得写抽象函数，能够看看这篇论文https://digitalcommons.utep.edu/cgi/viewcontent.cgi?referer=https://www.google.com.hk/&httpsredir=1&article=2073&context=cs_techrep ，我大概写了个抽象函数，没bug，但也没起做用，仍是报nodes没实现的错误，因此这里就不贴个人抽象函数了。

从上图能够看到若是不实现nodes，大多数方法都被skip掉了。

三. 架构设计

1. 第一次做业

直接继承接口，简单地实现了两个类。

2. 第二次做业

为了更改方便，直接ctrl+v把MyPathContiner的代码复制到MyGraph。

3. 第三次做业

因为第二次做业比较复杂，再去动极可能出bug，因而在写第三次做业的时候对于第二次做业已有的代码我一行都没动，只是在MyGraph类里加了求连通块个数的Public的函数。这样一来bug少了，但新加的架构和已有的架构看起来很不协调。

看了std码以后，惊呼：我以前竟将全部代码都直接放在src文件夹下。好的分层设计应该像标程同样，起码得有多个文件夹吧，好比base,core,util,grpha等。

四. bug和修复状况

三次做业均无bug。

五. 心得体会

撰写：规格的撰写用到了不少离散数学的知识，掌握常见的几种模式后，就可以比较容易地写出一些简单函数的规格。以我目前的水平看，写代码仍是要比写规格来得容易。

理解：实操中，我其实是先看的指导书，对于含混的地方，（好比起点和终点相同的状况下，算不算换乘，最小费用算多少？同一路径中若是有环该怎么算？）我会去详细阅读规格，由于规格严谨的描述了某一个方法该干什么。（但此次直觉上的理解实际上更靠谱，好比同一路径中有环的状况，直觉上的理解是不用非得绕着环走一圈多余的路，但死扣规格，确实得绕，过后证实是老师或助教的规格写错了）。

JML和JmlunitNG：JML设计指望过高，其目的是写出规格后，就能够自动生成测试用例，还可直接检查代码是否准确实现了规格；但相关工具链及其难用，功能及其有限，目前我只能写个简单的demo探索一下它的性质，体验一下整个流程。