OO第三單元——規格化設計與地鐵系統——總結

時間 2019-11-24

標籤第三單元規格化設計地鐵系統總結简体版

原文原文鏈接

OO第三單元——JML的使用與地鐵系統

梳理JML語言的理論基礎、應用工具鏈狀況

JML

The Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler.html

——https://en.wikipedia.org/wiki/Java_Modeling_Languagejava

jml，簡單來講，就是在每一個方法以前，相似於Javadoc，用註釋的形式寫出這個方法的效果。和其餘規格化是設計不一樣的是，它能夠算是使用了形式化的語言——這樣，咱們就可使用程序來解讀他，同時他也沒有了歧義性。node

他的基礎以下：git

使用註釋結構
由表達式構成
1. 原子表達式
  - 即各類特殊「符號（Symbol）」
  - 如 \result
2. 量化表達式
  - 如\forall \exists等
  - 基本格式相似於java中for的寫法，(\exist; condition; condition)能夠在裏面進行限制，約束。
  - 相似於 謂詞邏輯（離散數學）
3. 集合表達式
4. 操做符
方法規格
- 前置條件 (requires)
- 後置條件 (ensure)
- 反作用範圍限定 (assignable modifiable)
類型規格

參考：github

https://en.wikipedia.org/wiki/Java_Modeling_Languageweb

《JML Level 0手冊》算法

以上構成了jml的基礎緩存

JML工具鏈

A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations.bash

——https://en.wikipedia.org/wiki/Java_Modeling_Language架構

jml 須要支持一個編譯器jmlc，一個文檔生成器 jmldoc，一個單元測試程序jmlunit

如下團隊在作jml相關內容

ESC/Java2 [1], an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.

OpenJML declares itself the successor of ESC/Java2.

Daikon, a dynamic invariant generator.

KeY, which provides an open source theorem prover with a JML front-end and an Eclipse plug-in (JML Editing) with support for syntax highlighting of JML.

Krakatoa, a static verification tool based on the Why verification platform and using the Coq proof assistant.

JMLEclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.

Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.

JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.

TACO, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.

VerCors verifier

在Github和Gitlib搜索JML，大體得到了一下比較完善的開源項目實現：

OpenJML, 包含了編譯器等
JmlUnitNG，單元測試

JMLUnitNG 嘗試

這裏嘗試使用了一個較爲簡單的類

（有錯誤）

public class Alu {
    /*@
      @ ensures (a <= b) ==> (\result == a);
      @ ensures (a > b) ==> (\result == b);
      @*/
    public static int min(int a, int b) {
        return Integer.min(a, b);
    }
    /*@
      @ ensures (a >= b) ==> (\result == a);
      @ ensures (a < b) ==> (\result == b);
      @*/
    public static int max(int a, int b) {
        return Integer.min(a, b);
    }
}

分別運行

java -jar jmlunitng.jar Alu.java

javac -cp jmlunitng.jar *.java
java -jar openjml.jar -rac Alu.java

(注意這裏jmlunitng和openjml都只支持java8)

而後查看生成的文件

.
├── Alu.class
├── Alu.java
├── Alu_ClassStrategy_int.class
├── Alu_ClassStrategy_int.java
├── Alu_InstanceStrategy.class
├── Alu_InstanceStrategy.java
├── Alu_JML_Test.class
├── Alu_JML_Test.java
├── Alu_max__int_a__int_b__0__a.java
├── Alu_max__int_a__int_b__0__b.java
├── Alu_min__int_a__int_b__0__a.class
├── Alu_min__int_a__int_b__0__a.java
├── Alu_min__int_a__int_b__0__b.class
├── Alu_min__int_a__int_b__0__b.java
├── PackageStrategy_int.class
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String.class
├── PackageStrategy_java_lang_String.java
├── PackageStrategy_java_lang_String1DArray.class
└── PackageStrategy_java_lang_String1DArray.java

這裏閱讀這些文件，能夠注意到Jmlunitng生成的單元測試文件是使用TestNG測試的。

所以咱們使用TestNG測試。