Abstract

Introduction

This article is P12 of BUAA OO course, which integrates the work of us in JML section.

Firstly, we will introduce JML’s theory basement and tool chain. After that, we will show how we deploy and use the JML. Thirdly, we will analyze our project and its bugs. Finally, we will give a brief note of JML Syntax.

JML Introduction

This section introduce JML’s theory basement and tool chain.

Design by Contract

Design by contract (DBC) is a method for developing software ¹. The principal idea behind DBC is that a class and its clients have a “contract” with each other. The client must guarantee certain conditions before calling a method de?ned by the class, and in return the class guarantees certain properties that will hold after the call. The use of such pre- and postconditions to specify software dates back to Hoare’s 1969 paper on formal veri?cation ². What is novel about DBC is that it makes these contracts executable. The contracts are de?ned by program code in the programming language itself, and are translated into executable code by the compiler. Thus, any violation of the contract that occurs while the program is running can be detected immediately³

Behavioral Interface Speci?cation Language

Behavioral interface speci?cation languages provide formal code-level annotations, such as preconditions, postconditions, invariants, and assertions that allow programmers to express the intended behavior of program modules. Such speci?cations are useful for precisely documenting program behavior, for guiding implementation, and for facilitating agreement between teams of programmers in modular development of software. When used in conjunction with automated analysis and program veri?cation tools, such speci?cations can support detection of common code vulnerabilities, capture of light-weight application-speci?c semantic properties, generation of test cases and test oracles, and full formal program veri?cation.⁴

Java Modeling Language

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules.

JML combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.⁵

JML-Launcher⁶

The command jml-launcher starts a graphical user interface that can launch other JML tools. These include the JML checker (jml), the runtime assertion checking compiler (jmlc), the documentation generator (jmldoc), the specification skeleton generator (jmlspec), and the unit testing file generation tool (jmlunit).

The launcher can also be run by opening (double clicking) the file bin/jml-release.jar that is part of the JML release. The jar file and the script both run the Java class org.jmlspecs.launcher.JmlLauncher.

JML & JML-GUI⁷

The command jml and the graphical user interface version jml-gui both do type checking of Java Modeling Language (JML) specifications. JML is a behavioral interface specification language for Java(TM).

The jml script sets the CLASSPATH and then runs the Java class org.jmlspecs.checker.Main, which does both syntax and type checking of Java and JML files. That is it checks both Java source code and the JML annotations in source code and JML files.

The jml-gui script is similar, but just runs the Java class org.jmlspecs.checker.JmlGUI, which brings up a graphical user-interface to do the checking.

JMLC & JMLC-GUI⁸

The command jmlc and the graphical user interface jmlc-gui compile Java(TM) files (and JML specification files) with their JML annotations turned into runtime checks. It thus acts as a Java compiler, but with the additional effect of enabling automatic checks of assertions when the code is executed. The output is a .class file, which can be treated in much the same way as the output of any java compiler.

JMLDoc & JMLDoc-GUI⁹

The command jmldoc and the graphical user interface version jmldoc-gui generate HTML (web) pages from JML annotated Java(TM) and JML files. This is similar to Javadoc, but jmldoc understands JML specifications, and includes this information in the generated HTML pages. The program also type checks the JML specifications to some extent and combines annotations across refinement files. The output is a set of HTML files that can be browsed using a web browser.

OpenJML

OpenJML is a program verification tool for Java programs that allows you to check the specifications of programs annotated in the Java Modeling Language.¹⁰

OpenJML is capable of checking Java programs annotated with specifications in the Java Modeling Language and provides robust support for many of JML‘s features.

The goal of the OpenJML project is to implement a full tool for JML and current Java that is easy for practioners and students to use to specify and verify Java programs. In addition, the project seeks to advance the theory and experience of software verification in practical, industrially-relevant contexts.

OpenJML is not a theorem prover or model checker itself. OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. OpenJML supports major SMT solvers such as Z3, CVC4 and Yices. The success of the proofs will depend on the capability of the SMT solver (e.g., which logics it supports), the particular logical encoding of the code+specifications, and the complexity and style in which the code and specifications are written.

JML Editing

JML Editing extends the Java development tools (JDT) with support for JML to make writing JML specifications as convenient as writing Java source code.¹¹

AspectJML

The AspectJML tool is able to specify and do runtime assertion checking for both Java and AspectJ programs. Ajmlc uses aspect-oriented compilation techniques to provide significantly improved runtime assertion violation messages, and also works with JavaME.¹²

JML4C

The jml4c tool is a JML compiler built on the Eclipse Java compiler. It translates a significant subset of JML specifications into runtime checks.¹³

JML4c is a new JML compiler built upon the Eclipse JDT open-source platform; JML is a formal interface specification language for Java to document the behavior of Java classes and interfaces. It translates a significant subset of JML specifications into runtime checks.

Some of notable features of JML4c include

1. improved compilation speed
2. support for Java 5 features such as generics and enhanced for loops
3. support for nested classes
4. improved error messages

Using JML4c, therefore, one can now verify Java 5 classes annotated with JML specifications.

Sireum/Kiasan for Java

Sireum/Kiasan for Java is a JML contract-based automatic verification and test case generation tool-set for Java program units.¹⁴

JMLEclipse

JMLEclipse is a pre-alpha version of the JML tool-suite developed on top of Eclipse‘s JDT compiler infrastructure.¹⁵

JMLUnitNG

JMLUnitNG is an automated unit test generation tool for JML-annotated Java code, including code using Java 1.5+ features such as generics, enumerated types, and enhanced for loops. Like the original JMLUnit, it uses JML assertions as test oracles. It improves upon the original JMLUnit by allowing easy customization of data to be used for each method parameter of a class under test, as well as by using Java reflection to automatically generate test data of non-primitive types.¹⁶

JMLOK

JMLOK is a tool that uses random tests to check Java code against JML specifications and suggest likely causes for non-conformance problems it finds.¹⁷

AutoJML

AutoJML is a tool for the generation of JML specifications from state diagrams in various formats (including UML diagrams) and from security protocol specifications.¹⁸

AutoJML is a JML specification generator. It generates specifications based on other, higher level, specification formalisms such as UML state diagrams, or security protocol specifications. The output is a combination of Java skeleton code and JML class and method specifications.

SMT Solver Application Sample

We deploy and use the SMT Solver to analyse our project.

To Do (Unsolvable problem occurred during deploy SMT Solver.)

JML Application Sample

Because the specification of out project seems to be not compatible to the JMLUnit and OpenJML, we take a simple Java program as an example.

Download Dependencies

• OpenJML
  • ATTENTION: The release from home page is broken and somehow did not get fixed. We download from GitHub release page.

JML Syntax¹⁹

• Interface:

package daniel.jml.example;

// Refine Statement
//@ refine "<FileDir>"
// Import Statement
//@ model import org.jmlspecs.models.<JMLModel>;

import ...

interface MyInterface
{
    // Instance and Initially Statement
    /*@ public model instance <JMLModel> jmlModel;
      @ public initially <JMLExpression>;
      @*/

    // Invariant Statement
    /*@ public instance invariant <JMLExpression>;
    
    // Behavior Statement
    /*@ public normal_behavior
      @     requires <JMLExpression>;
      @     assignable <Variable>[, <Variable>]*;
      @     ensures <JMLExpression>;
      @ also
      @ public exceptional_behavior
      @     requires <JMLExpression>;
      @     signals_only <ExceptionClass>;
      @*/
    /*@ pure @*/ ReturnType method1(ArguType argu);
    
    // Behavior Statement
    /*@ public normal_behavior
      @     requires <JMLExpression>;
      @     assignable <Variable>[, <Variable>]*;
      @     ensures <JMLExpression>;
      @ also
      @ public exceptional_behavior
      @     requires <JMLExpression>;
      @     signals_only <ExceptionClass>;
      @*/
    ReturnType method2(ArguType argu);
}

JML

• Java Modeling Language
  • 用于对 Java 类型与接口进行规格化设计的行为接口规格语言 (Behavior Interface Specification Language)
    • Java 类型与接口: 合称 Java Module
    • 接口 Interface: 类型与接口的外部可见内容, 即API
    • 行为 Bahavior: 仅定义行为, 不限制实现
  • 提供对类型与接口的规格定义手段
• 能力
  • 可以基于规格自动构造测试用例
  • 可以对代码对规格的实现情况进行静态检查
• 用途
  • 规格化设计
  • 针对已有代码书写规格, 提高其可维护性
• 考虑到扩展性, JML分为多个层次 (Level)
  • Level 0: 核心语法, 要求所有工具均支持
• JML 由 Statement 组成
  • 同时包含文件中的 JML Statement 与 Java Statement

继承

• 当类型继承或实现另一个类型或接口时, 将自动继承其规格
• 使用also来连接本类中重写方法的规格与原有规格

class Class implements Interface
{
    /*@ also
      @ public normal_behavior
      @     ...
      @*/
    <ReturnType> method(<Argument>)
    {
        ...
    }
}

• 方法实现应满足继承链上所有对应规格

JML Interface

• JML 接口 JML Interface: Java Module (类型与接口) 的外部可见内容, 即API
  • 名称 (标识符)
    • 包名 (包路径)
    • 类型/接口名
    • 域名
    • 方法名
  • 类型
    • 域类型
    • 方法参数类型
    • 方法返回值类型
    • 方法抛出受查异常类型
  • 可见性
    • 类型/接口可见性
    • 域可见性
    • 方法可见性
• JML 将从类型与接口的定义中抽取其接口信息, 无需在 JML 中显式定义

JML Statement

• JML 以注释的形式表示规格, 称为 JML Statement
  • JML Statement 支持所有 Java 语句, 也有独有的扩展语句
  • 不能使用任何对变量赋值的语句
    • 不能使用非纯函数
  • 可使用修饰符 Modifier 修饰语句
• 放在注释对象之前
• 注释格式
  • 行注释: //@ <Statement>
    • 从@开始到行末的部分将被识别为 JML
  • 行内注释: /*@ <Statement> @*/
    • @之间的部分将被识别为 JML
  • 块注释:

/*@ <Statement>[
  @ <Statement>]*
  @*/

    - 注释块中每行从`@`开始到行末的部分将被识别为 JML

Instance Statement

//@ instance <Type> <Field>;

• Imagine that the Java Module (Class / Interface) has a field <Field> of type <Type>

//@ instance <Statement>;

• <Statement> become effective in the instance space, a imaginative space
• <Statement> is a JML Statement

Initially Statement

//@ instance <Type> <Field>;
//@ initially <JMLExpression>;

• Following a JML Instance Declaration Statement
• Assign that the field above in instance space (to client) satisfies <JMLExpression> initially

Invariant Statement

//@ invariant <JMLExpression>;

• Assign that the <JMLExpression> must be true all the time

Module Specification

• Specification for Java modules (Class / Interface)
• Should be under import statement

package ...
import ...

/*@ <Module Specification>[
  @ <Module Specification>]*
  @*/

Refine Statement

//@ refine "<RefinedFileDirectory>";

• Specify that current specification is a refinement of <RefinedFileDirectory>
  • Current specification adds to <RefinedFileDirectory>, by imposing additional constraints on <RefinedFileDirectory>
  • Existing specification is inherited
    • The method statements are inherited, and thus no need for repeating

Method Specification

• A correct implementation must satisfy all of the bahavior statements
• It is possible to only specify the public normal behavior, and not specify any exceptional behavior
  • Without Exceptional Behavior: For trusted client. Assume that requirement is always satisfied.
  • With Exceptional Behavior: For untrusted client.
• 常用方法
  • 分类讨论: 根据参数值的情况进行讨论

Normal_Behavior Statement

/*@ normal_behavior
  @     requires <JMLExpression>;
  @     assignable <Object>[, <Object>]*;
  @     ensures <JMLExpression>;
  @*/

• Specify a kind of method‘s normal behavior
• Prohibit throwing exception

Exceptional_Behavior Statement

/*@ exceptional_behavior
  @     requires <JMLExpression>;
  @     signals_only <ExceptionClass>;

• Specify a kind of method‘s exceptional bahavior
• Allow throwing exception

Also Statement

/*@     <BehaviorStatement>
  @ also
  @     <BehaviorStatement>

• Apposite Behavior Statements
  • Normal and Exceptional Bahavior can also be apposited
• For Apposited Behaviors, each must be obeyed when cooresponse precondition is true
• Can be used for override method to extends origin specification

@Override
/*@ also
  @ normal_behavior
  @     ...
  @*/
<ReturnType> method(<Argument>)
{
    ...
}

Old Statement

//@ old <Type> <Variable> = ...;

Require Statement

//@ requires <JMLExpression>;

• Give the method‘s precondition <JMLExpression>
  • Could be used for case analysis (分类讨论)
• Current behavior must be satisfied when precondition <JMLExpression> is satisfied by a call

Assignable Statement

//@ assignable <Variable>[, <Variable>]*;

• Only the fields listed and any on which they depend can be assigned to
  • Local variables, including the formal parameters of a method, and also fields of newly-created objects may be freely assigned by a method
  • Other than above, no other fields can be assigned
• Omitting the assignable statement means that all fields can be assigned
• Can use special <Variable>
  • \nothing

Ensure Statement

//@ ensures <JMLExpression>;

• Give the method‘s postcondition <JMLExpression>
• Calls to method must terminate in a state that satisfies the <JMLExpression>

Ensures_Redundantly Statement

//@ ensures_redundantly <JMLExpression>;

• State consequences of above specification
  • 解释在已有规格下运行结果将满足的状态: <JMLExpression>
  • 不添加额外规格, 仅解释已有规格
  • 可用于强调继承所得的, 已有, 但非可见的规格

Signals_Only Statement

//@ signals_only <ExceptionClass>;

• Give the method‘s exceptional postcondition <JMLExpression>
• Calls to method must terminate by throwing an instance of <ExceptionClass>

Java Statement

Import Statement

//@ import <FullClassName>;

• Has effect like a Java import statement for JML
• When use as a model statement
  • The import does not have to appear in an implementation like import ...

Statement Modifier

Model

• Model
  • 虚的, 无需具体实现
  • 仅用于 JML 规格描述
• JML 通过 声明 仅用于规格描述的 Model Field 来 描述 描述对象状态的 数学模型, 从而描述接口的行为
  • JML 通过 Model Field 来描述接口的行为
  • Model Field 仅用于描述规格, 无需 Java 实现
  • JML 定义了描述对象状态的数学模型
  • JML 通过描述该数学模型来描述接口行为
  • JML 通过 Model Field 来描述该数学模型
• Model or Non-Model
  • Model
    • 语句中包含model修饰符
    • 不需要 Java 实现
  • Non-Model
    • 语句中不包含model修饰符
    • 需要正确的 Java 实现

Public

• The statement is intended for clients

Pure

• 对方法

/*@ pure @*/ <ReturnType> <Method>(<Argument>)
{
    ...
}

- 要求方法是纯函数, 没有任何副作用
    - 不对任何外部变量赋值

• 对类型或接口

/*@ pure @*/ class <Class>
{
    ...
}

- 定义 Pure Type

Nullable

• 对参数

<RetuenType> method(/*@ nullable @*/ <Type> <Parameter>...)
{
    ...
}

- 当不使用`nullable`修饰符时, JML 会自动为所有behavior添加参数值非`null`的前置条件
    - JML 默认认为参数值不会为`null`
    - JML 默认不考虑参数值为`null`的情况
    - e.g.

/*@ public normal_behavior
  @     requires ...
  @     ...
  @ also
  @ public normal_behavior
  @     requires ...
  @     ...
  @*/
<ReturnType> method(<Type> arg1, <Type> arg2)
{
    ...
}

equivalent to:

/*@ public normal_behavior
  @     requires arg1 != null && arg2 != null;
  @     requires ...
  @     ...
  @ also
  @ public normal_behavior
  @     requires arg1 != null && arg2 != null;
  @     requires ...
  @     ...
  @*/
<ReturnType> method(<Type> arg1, <Type> arg2)
{
    ...
}

JML Expression

• Extended Java Expression
• Can be used in JML Statement
• If used in instance statement, the Expression can access objects in instance space

Forall Expression

\forall <Type> <Variable>; <Range>; <Condition>

• If every <Type> type variable <Variable> that satisfies first <JMLExpression>, it satisfies the second <JMLExpression> too, then return true; otherwise, return false.
  • If every <Type> type variable <Variable>, <JMLExpression> -> <JMLExpression> is true, return true; otherwise, return false.

Exist Expression

\exists <Type> <Variable>; <JMLExpression>; <JMLExpression>
\exists <Type> <Variable>; <Range>; <Condition>

• In all <Type> type variable <Variable> that satisfies first <JMLExpression>, there exists a variable that satisfies the second <JMLExpression> too

<==> Expression

<JMLExpression> <==> <JMLExpression>

• If and ONLY if
• Equivalent to == for boolean: <BooleanValue1> == <BooleanValue2> equivalent to <BooleanValue1> <==> <BooleanValue2>

Result Expression

\result

• Donate the return value of the method

Old Expression

\old(<JMLExpression>)

• Return the value of <JMLExpression> in pre-state of method

Not_Modified Expression

\not_modified(<JMLExpression>)

Java Expression

Pure Type

• Pure Type: Java classes that can be used as conceptual models in detailed design
  • Treated as purely immutable values in specification
  • Must pass certain conservative checks that make sure there is no possibility of observable side-effects from using such objects
• JML comes with a suite of pure types
  • Can be found in package org.jmlspecs.models

Define Pure Type

• Create pure types by giving a class or interface the pure modifier
• Written in .jml file
• Implements JMLType interface (?)
• Method
  • Specification Only: Contain method specifications without bodies
  • Pure Only: Should only have pure methods for JML Specification Usage
    • Each method is implicitly pure
      • can manually add redundant pure modifier
    • In JML, the use of non-pure method in an assertion is a type erroe
• Field
  • Model Only: Contain model field only

JMLType

• org.jmlspecs.models.JMLType
• Interface
• Method
  • clone()

/*@ also
  @ public normal_behavior
  @     ensures \result instanceof JMLType
  @         && ((JMLType) \result).equals(this);
  @*/
public /*@ pure @*/ Object clone();

- `equals(Object o)`

JML Package

• org.jmlspecs.models
  • Class:
    • Set
    • Sequence
    • Relation
    • Map
    • ...
  • All Classes are pure (side-effect free)
    • Can be used in assertions
      • Without affecting the state of the computation
      • Give assertions well-defined mathematical meaning
  • Useful for specification
  • Use usual Java syntax to invoke method

JMLValueSet

• A set that contains JMLType objects.

JML File

• .jml file
• Content understood by JML but not Java

Acknowledge

Reference

BUAAOO P9-P11 JML

原文：https://www.cnblogs.com/daniel10001/p/10908448.html