根据JML LEVEL 0手册梳理常用条目
对于含有JML注释的代码,可以使用如Openjml进行JML注释语法检查、静态检查、编译成支持rac的class文件。可以配合junitng自动化生成的测试用例对代码运行时正确性进行测试。
哪怕是复现讨论区中测试仍然菜出了许多问题,归结于原因为不是很了解java和javac寻找文件的方式,同时报错信息只有找不到***让人十分头大,最终笔者采用将Demo.java直接放到Openjml文件夹中才得以解决相关问题。
$ tree . |-- JMLTest.iml `-- openjml-0.8.42-20190401 |-- LICENSE.rtf |-- OpenJMLUserGuide.pdf |-- Solvers-linux | |-- cvc4-1.6 | |-- z3-4.3.0 | |-- z3-4.3.1 | `-- z3-4.7.1 |-- Solvers-macos | |-- cvc4-1.6 | |-- z3-4.3.1 | |-- z3-4.5.0 | |-- z3-4.6.0 | `-- z3-4.7.1 |-- Solvers-windows | |-- cvc4-1.6.exe | |-- z3-4.3.2.exe | `-- z3-4.7.1.exe |-- VERSION_INFO |-- epl-v10.html |-- jml-reference-manual.pdf |-- jmlruntime.jar |-- jmlspecs.jar |-- jmlunitng |-- jmlunitng.bat |-- jmlunitng.jar |-- openjml |-- openjml-template.properties |-- openjml.bat |-- openjml.jar `-- src `-- demo `-- Demo.java
第一步:jmlunitng生成测试代码
jmlunitng src/demo/Demo.java
$ tree . |-- LICENSE.rtf |-- OpenJMLUserGuide.pdf |-- Solvers-linux | |-- cvc4-1.6 | |-- z3-4.3.0 | |-- z3-4.3.1 | `-- z3-4.7.1 |-- Solvers-macos | |-- cvc4-1.6 | |-- z3-4.3.1 | |-- z3-4.5.0 | |-- z3-4.6.0 | `-- z3-4.7.1 |-- Solvers-windows | |-- cvc4-1.6.exe | |-- z3-4.3.2.exe | `-- z3-4.7.1.exe |-- VERSION_INFO |-- epl-v10.html |-- jml-reference-manual.pdf |-- jmlruntime.jar |-- jmlspecs.jar |-- jmlunitng |-- jmlunitng.bat |-- jmlunitng.jar |-- openjml |-- openjml-template.properties |-- openjml.bat |-- openjml.jar `-- src `-- demo |-- Demo.java |-- Demo_InstanceStrategy.java |-- Demo_JML_Data | |-- ClassStrategy_int.java | |-- ClassStrategy_java_lang_String.java | |-- ClassStrategy_java_lang_String1DArray.java | |-- compare__int_lhs__int_rhs__0__lhs.java | |-- compare__int_lhs__int_rhs__0__rhs.java | `-- main__String1DArray_args__10__args.java |-- Demo_JML_Test.java |-- PackageStrategy_int.java |-- PackageStrategy_java_lang_String.java `-- PackageStrategy_java_lang_String1DArray.java
第二步:javac 编译 JMLUnitNG 生成文件
javac -cp jmlunitng.jar -sourcepath src src/demo/**/*.java
$ tree . |-- LICENSE.rtf |-- OpenJMLUserGuide.pdf |-- Solvers-linux | |-- cvc4-1.6 | |-- z3-4.3.0 | |-- z3-4.3.1 | `-- z3-4.7.1 |-- Solvers-macos | |-- cvc4-1.6 | |-- z3-4.3.1 | |-- z3-4.5.0 | |-- z3-4.6.0 | `-- z3-4.7.1 |-- Solvers-windows | |-- cvc4-1.6.exe | |-- z3-4.3.2.exe | `-- z3-4.7.1.exe |-- VERSION_INFO |-- epl-v10.html |-- jml-reference-manual.pdf |-- jmlruntime.jar |-- jmlspecs.jar |-- jmlunitng |-- jmlunitng.bat |-- jmlunitng.jar |-- openjml |-- openjml-template.properties |-- openjml.bat |-- openjml.jar `-- src `-- demo |-- Demo.java |-- Demo_InstanceStrategy.java |-- Demo_JML_Data | |-- ClassStrategy_int.class | |-- ClassStrategy_int.java | |-- ClassStrategy_java_lang_String.class | |-- ClassStrategy_java_lang_String.java | |-- ClassStrategy_java_lang_String1DArray.class | |-- ClassStrategy_java_lang_String1DArray.java | |-- compare__int_lhs__int_rhs__0__lhs.class | |-- compare__int_lhs__int_rhs__0__lhs.java | |-- compare__int_lhs__int_rhs__0__rhs.class | |-- compare__int_lhs__int_rhs__0__rhs.java | |-- main__String1DArray_args__10__args.class | `-- main__String1DArray_args__10__args.java |-- Demo_JML_Test.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
第三步 :Openjml 编译
openjml -rac demo/Demo.java
$ tree . |-- LICENSE.rtf |-- OpenJMLUserGuide.pdf |-- Solvers-linux | |-- cvc4-1.6 | |-- z3-4.3.0 | |-- z3-4.3.1 | `-- z3-4.7.1 |-- Solvers-macos | |-- cvc4-1.6 | |-- z3-4.3.1 | |-- z3-4.5.0 | |-- z3-4.6.0 | `-- z3-4.7.1 |-- Solvers-windows | |-- cvc4-1.6.exe | |-- z3-4.3.2.exe | `-- z3-4.7.1.exe |-- VERSION_INFO |-- epl-v10.html |-- jml-reference-manual.pdf |-- jmlruntime.jar |-- jmlspecs.jar |-- jmlunitng |-- jmlunitng.bat |-- jmlunitng.jar |-- openjml |-- openjml-template.properties |-- openjml.bat |-- openjml.jar `-- src `-- demo |-- Demo.class |-- Demo.java |-- Demo_InstanceStrategy.java |-- Demo_JML_Data | |-- ClassStrategy_int.class | |-- ClassStrategy_int.java | |-- ClassStrategy_java_lang_String.class | |-- ClassStrategy_java_lang_String.java | |-- ClassStrategy_java_lang_String1DArray.class | |-- ClassStrategy_java_lang_String1DArray.java | |-- compare__int_lhs__int_rhs__0__lhs.class | |-- compare__int_lhs__int_rhs__0__lhs.java | |-- compare__int_lhs__int_rhs__0__rhs.class | |-- compare__int_lhs__int_rhs__0__rhs.java | |-- main__String1DArray_args__10__args.class | `-- main__String1DArray_args__10__args.java |-- Demo_JML_Test.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
第四步 :运行
java -cp jmlunitng.jar demo.Demo_JML_Test
[TestNG] Running: Command line suite Passed: racEnabled() Passed: constructor Demo() Passed: static compare(-2147483648, -2147483648) Failed: static compare(0, -2147483648) Failed: static compare(2147483647, -2147483648) Passed: static compare(-2147483648, 0) Passed: static compare(0, 0) Passed: static compare(2147483647, 0) Failed: static compare(-2147483648, 2147483647) Passed: static compare(0, 2147483647) Passed: static compare(2147483647, 2147483647) Passed: static main(null) Passed: static main({}) =============================================== Command line suite Total tests run: 13, Failures: 3, Skips: 0 ===============================================
对graph测试时由于相关原因没能引入规格,因此只进行了边界测试,结果如下(仅给出Fail Case):
[TestNG] Running: Command line suite ...... Passed Case ignored. Failed: <<MyGraph@47d384ee>>.getPathById(-2147483648) Failed: <<MyGraph@2d6a9952>>.getPathById(0) Failed: <<MyGraph@22a71081>>.getPathById(2147483647) Failed: <<MyGraph@3930015a>>.getPathId(null) Failed: <<MyGraph@629f0666>>.getShortestPathLength(-2147483648, -2147483648) Failed: <<MyGraph@1bc6a36e>>.getShortestPathLength(0, -2147483648) Failed: <<MyGraph@1ff8b8f>>.getShortestPathLength(2147483647, -2147483648) Failed: <<MyGraph@387c703b>>.getShortestPathLength(-2147483648, 0) Failed: <<MyGraph@224aed64>>.getShortestPathLength(0, 0) Failed: <<MyGraph@c39f790>>.getShortestPathLength(2147483647, 0) Failed: <<MyGraph@71e7a66b>>.getShortestPathLength(-2147483648, 2147483647) Failed: <<MyGraph@2ac1fdc4>>.getShortestPathLength(0, 2147483647) Failed: <<MyGraph@5f150435>>.getShortestPathLength(2147483647, 2147483647) Failed: <<MyGraph@1c53fd30>>.isConnected(-2147483648, -2147483648) Failed: <<MyGraph@50cbc42f>>.isConnected(0, -2147483648) Failed: <<MyGraph@75412c2f>>.isConnected(2147483647, -2147483648) Failed: <<MyGraph@282ba1e>>.isConnected(-2147483648, 0) Failed: <<MyGraph@13b6d03>>.isConnected(0, 0) Failed: <<MyGraph@f5f2bb7>>.isConnected(2147483647, 0) Failed: <<MyGraph@73035e27>>.isConnected(-2147483648, 2147483647) Failed: <<MyGraph@64c64813>>.isConnected(0, 2147483647) Failed: <<MyGraph@3ecf72fd>>.isConnected(2147483647, 2147483647) Failed: <<MyGraph@483bf400>>.removePathById(-2147483648) Failed: <<MyGraph@21a06946>>.removePathById(0) Failed: <<MyGraph@77f03bb1>>.removePathById(2147483647) Failed: <<MyGraph@326de728>>.removePath(null) =============================================== Command line suite Total tests run: 43, Failures: 26, Skips: 1 ===============================================
可以看到测试主要数据由0、null、MAX、MIN等边界数据构成。
原文:https://www.cnblogs.com/ShadowAlex/p/10908455.html