首页 > 其他 > 详细

OO 第三单元总结

时间：2019-05-22 21:46:47      阅读：110      评论：0      收藏：0      [点我收藏+]

1. JML梳理

根据JML LEVEL 0手册梳理常用条目

1.1 JML 理论基础

  • \result表达式 ： 表示方法返回值
  • \old( expr )表达式：表示方法执行之前expr表达式取值，若expr为相关引用，只能判断引用本身是否发生了变化
  • \type(type)表达式：返回类型type对应的类型。
  • \typeof(expr)表达式：该表达式返回expr对应的准确类型。
  • \forall表达式：(\forall int i ;  exprA ; exprB)  通俗理解为 ∀i(exprA -> exprB)
  • \exists表达式: (\forall int i ;  exprA ; exprB)   通俗理解为 ∃i(exprA -> exprB)　　
  • 前置条件(pre-condition) : requires expr
  • 后置条件(post-condition) : ensures expr
  • 副作用范围限定(side-effects) : assignable、modifiable
  • 正常功能 ：public normal behavior
  • 异常功能 ：public exceptional_behavior
  • 抛出异常 ： signals
  • 不变式invariant : 要求在所有可见状态下都必须满足的特性
  • 状态变化约束constraint : 对象状态变化是两次满足的一定约束，不变式的子集。

 

1.2 JML应用工具链

 　　对于含有JML注释的代码，可以使用如Openjml进行JML注释语法检查、静态检查、编译成支持rac的class文件。可以配合junitng自动化生成的测试用例对代码运行时正确性进行测试。

 

2. JMLUnitNG自动生成测试尝试

２.１首先是讨论区大佬给出样例的复现

　　哪怕是复现讨论区中测试仍然菜出了许多问题，归结于原因为不是很了解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 进行测试

对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
===============================================
Graph边界测试结果

可以看到测试主要数据由0、null、MAX、MIN等边界数据构成。

3.架构设计

3.1 Project 9

　　技术分享图片

　　

　　3.1 Project 9

OO 第三单元总结

原文：https://www.cnblogs.com/ShadowAlex/p/10908455.html
踩
(0)
赞
(0)
   
举报
评论 一句话评论（0）
分享档案
更多>
2021年09月23日 (328)
2021年09月24日 (313)
2021年09月17日 (191)
2021年09月15日 (369)
2021年09月16日 (411)
2021年09月13日 (439)
2021年09月11日 (398)
2021年09月12日 (393)
2021年09月10日 (160)
2021年09月08日 (222)
最新文章
更多>
教程昨日排行
更多>
友情链接
汇智网   PHP教程   插件网  
关于我们 - 联系我们 - 留言反馈 - 联系我们:wmxa8@hotmail.com
© 2014 bubuko.com 版权所有
打开技术之扣，分享程序人生！