一、JML理论基础

1.概览

在概述JML之前我想我们应该首先了解契约式设计（Design by Contract, DbC）。DbC要求在软件程序设计时明确每一个模块单元在调用前后的状态变化，抽象出来就是要求明确前置条件、后置条件和不变式。和诸多设计模式一样，DbC可以说是一种方法学，一种软件开发和程序设计的规范化操作。Eiffel语言是第一个在语法层面上要求做到DbC的语言，自此之后在软件和程序设计领域专门针对DbC的实践也越来越多，事实上JML就是其中之一。

JML（Java Modeling Language）是行为接口规范语言（behavioral interface specification language, BISL）的一种，它的主要作用是使用Java的语法去规范类、方法接口以及抽象数据的行为，进而达到契约式设计的目的。

JML本身是建立在形式化验证语言工具Larch、断言检查以及Eiffel语言的契约式设计方法之上的，但它也有不少新特性。比如，相比于Larch在规约中表现的语言无关（language-independent）的特点，JML在断言中都使用的是Java的表达式语法，这无疑大大增强了JML对Java语言规约的表达能力，同时也减少了程序员的学习成本。又比如，JML中支持诸如/forall和/exist这样的量词以及model修饰的仅用于规格描述的属性，这使得JML可以给出比Eiffel更为精确的规约描述。

JML在设计时有两个重要目标：一是使得它本身对于任何Java程序员都容易理解，这一点上一段中已经提及；二是JML本身不会去规定——或者说强制指明任何方法的实现，相反，它应该能够描述以任何可能的实现方式设计的方法，这一点我想通过作业就能有所体会。

2.JML基本语言特征

下面是一个使用JML的简单例子：

public interface Wallet {
    /*@ public instance model non_null int moneySum;
      @ public instance model non_null int[] faceVal;
      @*/

    /*@ invariant (faceVal.length == 0 && moneySum == 0) ||
      @     (moneySum == (\sum int i; 0 <= i && i <= faceVal.length; faceVal[i]))
      @*/

    //@ ensures \result == moneySum;
    public /*@pure@*/ int getMoneySum();

    /*@ public normal behaviour
      @ requires val > 0;
      @ assignable moneySum, faceVal;
      @ ensures moneySum == \old(moneySum) + val;
      @ ensures faceVal.length == \old(faceVal.length) + 1;
      @ ensures (\forall int i; 0 <= i && i < \old(faceVal.length);
      @         faceVal[i] == \old(faceVal[i]));
      @ ensures faceVal[faceVal.length - 1] == val;
      @ also
      @ public exceptional behaviour
      @ signals (WrongValueException e) val <= 0;
      @*/
    public void addNewVal(int val);

    /*@ public normal behaviour
      @ requires val > 0;
      @ requires (\exists int i; 0 <= i && i <= faceVal.length; faceVal[i] == val);
      @ assignable moneySum, faceVal;
      @ ensures moneySum == \old(moneySum) - val;
      @ ensures faceVal.length == \old(faceVal.length) - 1;
      @ ensures (\forall int i; 0 <= i && i < \old(faceVal.length) && \old(faceVal[i] != val);
      @         (exists int j; 0 <= j && j < faceVal.length; faceVal[j] == \old(faceVal[i]));
      @ ensures (\sum int i; 0 <= i && i < faceVal.length && faceVal[i] == val; 1) ==
      @         (\sum int j; 0 <= j && j < \old(faceVal.length) && \old(faceVal[j] == val); 1) - 1;
      @ also
      @ public exceptional behaviour
      @ signals (WrongValueException e) val <= 0;
      @ signals (NoSuchFaceValueException e) !(\exists int i; 0 <= i && i <= faceVal.length; faceVal[i] == val);
     */
    public void costVal(int val);
}

可以看到JML的语法和Java语言本身是十分相近的，但JML相比于Java语言仍扩充了一些关键字用来描述规约。从该代码实例中当中可以梳理出JML的基本语法特征；

　　①JML的主体部分和DbC的要求一样，分为前置条件、后置条件和不变式，它们分别通过/requires、/ensures、invariant来标识；

　　②JML支持normal和exceptional的后置条件，后者可以使用signals字句标识并指明导致异常的条件；

　　③JML中定义了一些Java中并不包含的符号，如例子中的/forall、/exists；此外JML还定义了逻辑运算符==>、<==>等，这些定义可以使得JML更好的描述规格；

　　④assignable可以用来指明方法仅给哪些变量或对象赋值；

　　⑤model修饰的属性仅包含抽象意义，它仅用来使得规格能够对具体实现进行抽象地描述，实际在实现时并不一定会定义model修饰的属性；

　　⑥被pure修饰的方法没有任何可见的副作用，比如例子中的get方法；被pure修饰的方法也可出现在其他断言中。

JML还有很多其他内容，具体可查阅其官方参考手册。

二、工具链应用

1.OpenJML

根据OpenJML工具官网的描述，它可以把JML转换为SMT-LIB格式，并将其中隐含的证明问题传递给后端的SMT Solver。因此这里我直接使用OpenJML来尝试验证规格与规格实现。

环境配置方面，我使用的是Win10系统，并安装、配置了jdk1.8.0版本，在OpenJML官网的下载页面下载了OpenJML命令行工具后即可使用OpenJML。

尝试直接去使用课程组提供的JML进行验证，发现OpenJML会直接报告Internal Bug。于是我写了下面这个简单的类来尝试使用OpenJML，该类里定义了一个和作业中Group接口里的getAgeMean方法功能相同的方法（规格作了一定修改），并写了一个简单的内部类Person。

public class OpenJmlTest {
    private class Person {
        private int id;
        private int age;

        public Person(int _id, int _age) {
            id = _id;
            age = _age;
        }

        public int getAge() {
            return age;
        }

        public int getId() {
            return id;
        }
    }
    
    private /*@spec_public@*/ List<Person> people = new ArrayList<Person>();
      
    /*@ ensures \result == (people.size() == 0? 0 :
      @          ((\sum int i; 0 <= i && i < people.size(); people.get(i).getAge()) / people.size()));
      @*/
    public /*@pure@*/ int getAgeMean() {
        int ageSum = 0;
        for (int i = 0; i < people.size(); i++) {
            ageSum += people.get(i).getAge();
        }
        return ageSum / people.size();
    }
}

OpenJML工作时默认使用其支持最好的Z3求解器，可以直接使用类似于下面的命令进行静态检查：

java -jar .\openjml.jar -esc OpenJmlTest.java

检查结果如下：

OpenJmlTest.java:27: 警告: A non-pure method is being called where it is not permitted: OpenJmlTest.Person.getAge()
@ ((\sum int i; 0 <= i && i < people.size(); people.get(i).getAge()) / people.size()));
^
OpenJmlTest.java:27: 警告: NOT IMPLEMENTED: Not yet supported feature in converting BasicPrograms to SMTLIB: JML Quantified expression using \sum
@ ((\sum int i; 0 <= i && i < people.size(); people.get(i).getAge()) / people.size()));
^

OpenJmlTest.java:32: 警告: The prover cannot establish an assertion (Assignable: OpenJmlTest.java:26: 注: ) in method getAgeMean: \everything
ageSum += people.get(i).getAge();
^
OpenJmlTest.java:26: 警告: Associated declaration: OpenJmlTest.java:32: 注:
/*@ ensures \result == (people.size() == 0? 0 :
^
OpenJmlTest.java:34: 警告: The prover cannot establish an assertion (PossiblyDivideByZero) in method getAgeMean
return ageSum / people.size();
^

OpenJmlTest.java:32: 警告: The prover cannot establish an assertion (ArithmeticOperationRange) in method getAgeMean: overflow in int sum
ageSum += people.get(i).getAge();
^

OpenJmlTest.java:32: 警告: The prover cannot establish an assertion (ArithmeticOperationRange) in method getAgeMean: underflow in int sum
ageSum += people.get(i).getAge();

第一个警告说明在规格中使用了未声明为pure的方法getAge()。

第二个警告说明\sum还不被支持，事实上OpenJML目前并不能对JML支持的很好，对于复杂的JML常常无力处理，这和OpenJML的更新滞后以及SMT Solver的功能都有关系。

第三个警告中出现了Assignable，猜测是在语句 ageSum += people.get(i).getAge(); 中可能存在赋值错误，同时第四条警告指出与之相关的规格语句是ensures子句。为了了解原因，重新加上 -subexpressions参数让OpenJML输出更为详细的测试过程，摘取相关的输出如下：

OpenJmlTest.java:32: 注:        ageSum += people.get(i).getAge()
                        VALUE: people    === REF!val!19
                        VALUE: i         === 609
                        VALUE: people.get(i)     === REF!val!30
                        VALUE: people.get(i).getAge()    === 0
                        VALUE: ageSum += people.get(i).getAge()  === 0
OpenJmlTest.java:32: 注:        PossiblyNullDeReference assertion: _JML__tmp90 != null
...

  

  OpenJmlTest.java:32: 注: PossiblyNullDeReference assertion: _JML__tmp128 != null
  OpenJmlTest.java:1: 注: Precondition assertion: _$CPRE__11
  　　　　　　　　　　　　VALUE: _$CPRE__11 === true
  OpenJmlTest.java:14: 注: Assignable assertion: _JML__tmp132 || (!Pre_5 || false)
　　　　　　　　　　　　　VALUE: false === false
　OpenJmlTest.java:32: 注: Invalid assertion (Assignable)
 : OpenJmlTest.java:26: 注: Associated location

根据输出，猜测OpenJML认为这里的赋值可能存在空引用的错误，所以给了Assignable警告。

第五条警告说明当people.size()为0时将发生除0错误，显然这里没有遵照规格中对people.size()等于0时的处理。

第六、七条警告出现了ArithmeticOperationRange，说明在累加的过程中可能导致ageSum的溢出。

根据上述警告可以对getAgeMean进行修改：

　　/*@ ensures \result == (people.size() == 0? 0 :
      @          ((\sum int i; 0 <= i && i < people.size(); people.get(i).getAge()) / people.size()));
      @*/
    public /*@pure@*/ int getAgeMean() {
        if (people.size() == 0) {
            return 0;
        }
        long ageSum = 0;
        for (int i = 0; i < people.size(); i++) {
            ageSum += people.get(i).getAge();
        }
        return ((int) ageSum / people.size());
    }

修改后进行静态检查仍会有警告，但认为规格的要求已经达到，遂忽略这些警告。关于OpenJML给出的警告信息含义可以查看其官方说明，或者查看OpenJML User Guide。OpenJML的作用确实有限，不过或许可以学习OpenJML是如何把JML转换为SMT Solver可以求解的SMT-LIB格式的。

2.JMLUnitNG

JMLUnitNG可在官网获得下载和资料。将Group.java、Person.java、MyGroup.java和MyPerson.java置于一个文件夹下，在该目录下依次运行以下命令：

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

可以得到对MyGroup的测试结果如下：

[TestNG] Running:
  Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Passed: <<MyGroup@64cee07>>.addPerson(null)
Passed: <<MyGroup@1761e840>>.addPerson(null)
Passed: <<MyGroup@5ecddf8f>>.addPerson(null)
Passed: <<MyGroup@3f102e87>>.delPerson(null)
Passed: <<MyGroup@27abe2cd>>.delPerson(null)
Passed: <<MyGroup@5f5a92bb>>.delPerson(null)
Passed: <<MyGroup@6fdb1f78>>.equals(null)
Passed: <<MyGroup@51016012>>.equals(null)
Passed: <<MyGroup@29444d75>>.equals(null)
Passed: <<MyGroup@2280cdac>>.equals(java.lang.Object@1517365b)
Passed: <<MyGroup@4fccd51b>>.equals(java.lang.Object@44e81672)
Passed: <<MyGroup@60215eee>>.equals(java.lang.Object@4ca8195f)
Passed: <<MyGroup@65e579dc>>.getAgeMean()
Passed: <<MyGroup@61baa894>>.getAgeMean()
Passed: <<MyGroup@768debd>>.getAgeMean()
Passed: <<MyGroup@490d6c15>>.getAgeVar()
Passed: <<MyGroup@7d4793a8>>.getAgeVar()
Passed: <<MyGroup@449b2d27>>.getAgeVar()
Passed: <<MyGroup@5479e3f>>.getConflictSum()
Passed: <<MyGroup@27082746>>.getConflictSum()
Passed: <<MyGroup@66133adc>>.getConflictSum()
Passed: <<MyGroup@7bfcd12c>>.getId()
Passed: <<MyGroup@42f30e0a>>.getId()
Passed: <<MyGroup@24273305>>.getId()
Passed: <<MyGroup@46f5f779>>.getRelationSum()
Passed: <<MyGroup@1c2c22f3>>.getRelationSum()
Passed: <<MyGroup@18e8568>>.getRelationSum()
Passed: <<MyGroup@33e5ccce>>.getValueSum()
Passed: <<MyGroup@5a42bbf4>>.getValueSum()
Passed: <<MyGroup@270421f5>>.getValueSum()
Passed: <<MyGroup@52d455b8>>.hasPerson(null)
Passed: <<MyGroup@4f4a7090>>.hasPerson(null)
Passed: <<MyGroup@18ef96>>.hasPerson(null)
Passed: <<MyGroup@6956de9>>.peopleSum()
Passed: <<MyGroup@769c9116>>.peopleSum()
Passed: <<MyGroup@6aceb1a5>>.peopleSum()

===============================================
Command line suite
Total tests run: 40, Failures: 1, Skips: 0
===============================================

在构造方法里传入了一些边界值，此外有几个方法都传入了null，可以看出JMLUnitNG在测试时会有意针对边界情况。

三、作业分析

1.第一次作业

本次作业类图如下：

实现时仅新建了MyPerson和MyNetwork两个类：

本次作业比较简单，在架构设计方面并没有需要考虑的地方。算法方面，仅在MyNetwork的isCircle方法中使用了Dijkstra，其余方法的实现均和规格中的描述大致相同。

2.第二次作业

本次作业类图如下：

工程组织如下：

本次作业新增了Group接口，Network中也新增了有关方法。由于有明确的性能限制，直接照抄规格已不可行。我首先考虑的是优化Network类的isCircle方法，经查阅资料了解到了可以十分方便且高效的并查集算法，同时考虑到后续可能新增更多与图论算法相关的内容，于是新增了DisjointPersonSet这个类，其中主要内容就是实现并查集。此外我进行的优化是针对Group接口中的getAgeMean、getAgeVar、getRelationSum和getValueSum四个方法，优化思路是在每次进行addPerson操作时更新当前Group中所有人的年龄和、所有人的年龄平方和、所有人的relation数量以及value总和。其中需要注意的点包括年龄和或平方和的溢出问题、对已在组内的两个人加入新relation时对relationSum和valueSum的更新问题。事实上Network中的getNameRank方法也非常值得优化，但我此次作业没有去尝试。

本次作业并未直接根据JML去实现所有方法，而是以自己的设计为准。但是在模型构建方面我并没有进行过多考虑，仅仅是把所有person以及他们之间的relation视作一整个图去建模，在课上讲解中提到的动态更新图结构这一点我没有考虑到。

3.第三次作业

本次作业类图如下：

工程组织如下：

 

本次作业在Network接口中新增了若干高复杂度的方法，我的优化方案如下：

　　1.为优化queryNameRank方法，实现了红黑树的数据结构，当进行addPerson操作时就将新person的name插入到红黑树中；当询问排名时，根据红黑树中左右孩子大小关系去计算排名，但要注意重名的情况（可以给每个节点设置一个变量记录重复次数）；

　　2.为优化queryAgeSum方法使用了线段树管理所有age；

　　3.为优化queryMinPath方法采用了堆优化的Dijkstra；

　　4.为优化queryStrongLinked方法采用Tarjan算法求点双连通分量；

　　5.为优化queryBlockSum方法使用了并查集，当执行addPerson操作时blockSum值加1，当并查集中执行一次合并操作时blockSum值减1，而当调用queryBlockSum方法时直接返回blockSum的值即可。

上述1部分我在NameDir类中进行了实现，2部分在MyNetwork中实现，其余部分均在PersonSet类中实现。最终的MyNetwork类只需实例化NameDir对象和PersonSet对象并调用它们的方法来完成Mynetwork自身的方法。由于实现内容多，我重新考虑了工程结构，把MyPerson类和PersonSet类放在了people包下，把MyGroup、MyNetwork和NameDir三个类放在了network包下，以此区分这些类承载的不同功能。

这次实现并未直接去根据JML实现所有方法。但是在模型构建上也存在和作业二一样的问题，并且此次作业我更多的是围绕某个局部算法下功夫，对于这个图有什么特点、如何去描述这些特点都没有足够的思考。

四、Bug情况

第一次作业中没有出现Bug。

第二次作业中我没有在addRelation的时候动态维护每个Group中的relationSum和valueSum，导致强测和互测中出现很多点WA掉。

第三次作业中，我在实现线段树的时候把年龄范围手误写错了，导致许多点WA掉；此外我在开始实现queryStrongLinked方法时没有采用Tarjan算法而是使用DFS判断环，这导致了TLE。

五、心得体会

我认为在理解和编写JML规格的过程中核心就在于前置条件、后置条件和不变式三个概念的把握。用户的需求是通过后置条件体现的，实现者需要用户去满足的要求是通过前置条件体现的，而对某个对象本身状态和对象间关系的要求则是通过不变式去体现的。在我看来JML是从过程和关系的角度去描述软件或程序的实现的，它把这样的过程和关系抽象成为了用户、实现者和被操作对象这三者之间的“互动”规则。

初次学习JML时就认为这是一种相当有用的工具，使用它可以克服掉软件和程序设计中过程中的一些不必要的麻烦和错误。后续通过进一步地学习了解到了JML实际上是DbC思想在Java语言上的一种实现，在JML之前类似的实现就已经在Eiffel、C++等语言上进行过了。回想起之前所学习的设计模式，乃至面向对象程序设计本身，它们都是从人们长期积累的经验之中抽象出来的思想的概括和总结。