OpenJML入門

目錄

• OpenJML 獲取
  • 下載
  • 使用
    • Linux
    • Windows
• Parsing and Type-checking
• Extended Static Checking
• Runtime Assertion Checking
• 參考

OpenJML 獲取

下載

OpenJML下載可以通過其github倉庫獲取。傳送門

使用

下載完成后，可以直接使用命令行進行操作，但是比較麻煩。這里提供兩個版本的輔助文件簡化操作

Linux

# filename : openjml
#!/bin/bash
java -jar path/to/openjml.jar "$@"

其中jar包的路徑需要自行修改。

Windows

::openjml.bat
@echo off

set java=java -jar "%~dp0openjml.jar" -noPurityCheck
set prove=-prover cvc4 -exec "%~dp0Solvers-windows\cvc4-1.6.exe"
set runtime=-cp %~dp0jmlruntime.jar;

set allparam=
set rac=

:param
set str=%1
if "%str%"=="" (
    goto end
)
if "%str%"=="-rac" (
	set rac=rac
)
if "%str%"=="-prove" (
	set str=%prove%
)
set allparam=%allparam% %str%
shift /0
goto param

:end
if "%allparam%"=="" (
    goto eof
)

rem remove left right blank
:intercept_left
if "%allparam:~0,1%"==" " set "allparam=%allparam:~1%"&goto intercept_left

:intercept_right
if "%allparam:~-1%"==" " set "allparam=%allparam:~0,-1%"&goto intercept_right

:eof
%java% %allparam%
set filename=
if "%rac%"=="rac" (
	:input
	set /p filename=Input file name:
	if "%filename%"=="" (
		goto input
	)
	java %runtime% %filename%
)


pause

用戶可以將上述代碼拷貝到解壓后的文件夾中，然后將該文件夾加入環境變量。即可通過命令行調用openjml命令了。這里為了簡化驗證時的參數傳遞，提供了一個-prove參數。用戶指定這一參數后，程序將選定prover並執行。

Parsing and Type-checking

OpenJML最基本的功能就是對JML注釋的完整性進行檢查。檢查包括經典的類型檢查、變量可見性與可寫性等。通過命令行使用OpenJML時，可以通過-check參數（缺省）指定類型檢查。

openjml [-check] options files

舉例來說

public class main {
	/*@
	  @ require args != null
	  @*/
	public static void main(String[] args) {
		System.out.println(args);
	}
}

運行語法檢查后報錯

C:\>openjml main.java
main.java:17: 錯誤: 需要';'
          @ require args != null
                        ^
main.java:17: 錯誤: 找不到符號
          @ require args != null
            ^
  符號:   類 require
  位置: 類 main
2 個錯誤

類型檢查檢測出了注釋中的兩處錯誤。分別更改后的程序如下

public class main {
	/*@
	  @ requires args != null;
	  @*/
	public static void main(String[] args) {
		System.out.println(args);
	}
}

再次運行后即可通過檢查。

Extended Static Checking

類型檢查只能確保jml注釋的格式正確，但是對規格內容不進行檢查。下述程序中明顯違背了規格的描述，但是類型檢查仍然通過了。

public class main {
	/*@
	  @ requires a != 0 && b != 0;
	  @ ensures \result <= 1 && \result >= 0;
	  @*/
	public static int fun(int a, int b) {
		return a > b ? 1 : 0;
	}
	public static void main(String[] args) {
		fun(1, 0);
	}
}

為了對規格內容進行檢查，需要使用-esc參數

C:\>openjml -esc -prove main.java
main.java:10: 警告: The prover cannot establish an assertion (Precondition: main.java:6: 注: ) in method main
                fun(1, 0);
                   ^
main.java:6: 警告: Associated declaration: main.java:10: 注:
        public static int fun(int a, int b) {
                          ^
main.java:3: 警告: Precondition conjunct is false: b != 0
          @ requires a != 0 && b != 0;
                                 ^
3 個警告

這里需要注意，靜態檢查需要指定prover。在上述Windows版的批處理函數中，默認指定了一個prover。用戶也可以使用-prover等參數指定自定義檢查器。

那么esc是如何完成的呢？好奇的話可以通過-progress參數或-verboseness參數來查看檢查的具體過程。下面截取了部分輸出

C:\>openjml -esc -prove main.java -verboseness=3
...
STARTING PROOF OF main.main(java.lang.String[])
/*@
  public behavior
    requires args != null;
    signals_only java.lang.RuntimeException;
    assignable \everything;
    accessible \everything;
 */

{
  fun(1, 0);
}
...

可以看出OpenJML在驗證前會首先重整規格，而后針對性生成測試程序。由於生成程序過長，可以在本地嘗試。此處使用的是-verboseness=3，如果使用 4 將會輸出大量信息。

Runtime Assertion Checking

使用-rac選項可以執行運行時檢查。上述批處理文件中存在 bug，第一次輸入文件名時可能會要求再次輸入。

C:\>openjml -rac main.java
Input file name:main
main.java:10: 警告: JML precondition is false
                fun(1, 0);
                   ^
main.java:6: 警告: Associated declaration: main.java:10: 注:
        public static int fun(int a, int b) {
                          ^

這時會自動運行生成出來的.class文件，但經過反匯編后我的.class文件並不能編譯。因此目前還沒有看懂rac的具體流程。此外，-rac選項有許多補充選項，功能十分豐富，大家可以多多嘗試。

參考

OpenJML 基本使用 倫澤標