OO第三单元总结

前言

本单元中，初次接触到了The Java Modeling Language (JML)这种语言，主要尝试了根据规格进行相应代码实现，及根据代码或需求抽象出相应规格的练习。从PathContainer，Graph到RailwaySystem，一路发展过来，在实现这些接口的新方法时，都是按照方法规格进行了代码实现。同时，也尝试了通过规格来进行一定的形式化验证。

一、JML语言

（1）JML语言的理论基础

JML是一种形式化的、面向JAVA的行为接口规格语言

JML允许在规格中混合使用Java语法成分和JML引入的语法成分

JML使用Javadoc的注释方式

• 结构化、扩展性强

• 块注释：/@ … @/

• 行注释：//@

JML语法

• Precondition

    • /*@ requires P; @*/

• Postcondition

    • /*@ ensures P; @*/

• Side-Effects

    • /*@ assignable list;@*/

• Exception

    • /*@ signal (Exception e) P;@*/

• Invariant

    • /*@ invariant P; @*/

• Constraint

    • /*@ constraint P; @*/

• method result reference

    • 
esult

• Previous expression value

    • old(E)

Using private fields in specifications

    private /*@ spec_public @*/ Type property;

Fields not null

    Private /*@ not_null @*/ Type property;

Declare spec variable

    //@ public model Type x;

Quantifiers

Iterating over all variables

    (forall T x; R(x); P(x))

Verifying if exist variables

    (exists T x; R(x); P(x))

Num of elements

    (
um_of T x; R(x); P(x))

Sum of expression

    (sum T x; R(x); E)

方法规格抽象

• 执行前对输入的要求----前置条件(precondition)

• 执行后返回结果应该满足的约束----后置条件(postcondition)

数据规格抽象（类型抽象）

• 数据状态应该满足的要求----不变式(invariant)

• 数据状态变化应该满足的要求----约束(constraint)

（2）应用工具链

OpenJML

OpenJML能够检查Java Modeling Language中使用规范注释的Java程序，并为JML的许多功能提供强大的支持。

OpenJML中的验证可以通过使用我们的扩展静态检查工具或使用我们的运行时断言检查功能来执行。运行时断言检查通常更容易编写规范，而静态检查可以更好地保证程序行为。

OpenJML不是定理证明器或模型检查器本身。OpenJML将JML规范转换为SMT-LIB格式，并将Java + JML程序隐含的证明问题传递给后端SMT求解器。与最流行的SMT解算器集成。

JMLUnitNG

JMLUnitNG是一个用于JML注释的Java代码的自动化单元测试生成工具，包括使用Java 1.5+特性的代码，例如泛型，枚举类型和增强的for循环。与原始的JMLUnit一样，它使用JML断言作为测试oracles。它通过允许轻松定制要用于测试类的每个方法参数的数据，以及使用Java反射自动生成非基本类型的测试数据，改进了原始JMLUnit。

......

二、JMLUnitNG测试

测试Path接口实现

package demo;

import java.util.ArrayList;

public class Test {
    public ArrayList<Integer> nodes = new ArrayList<Integer>();

    /*@ public normal_behavior
      @ ensures 
esult == nodes.size();
      @*/
    public /*@pure@*/ int size() {
        return nodes.size();
    }
    
    public static void main(String[] args) {
        Test t1 = new Test();
        t1.nodes.add(2);
        t1.nodes.add(1);
        t1.nodes.add(4);
        t1.nodes.add(7);
    }
}