BUAAOO Unit3 JML形式化方法

JML(Java modeling language) 是一种利用形式化描述对数据、方法进行约束的语言,包含数据规格、方法规格、迭代器规格。通过JML的形式化描述,建立功能、开发者、程序之间的契约,可以对程序扩展时的稳定性、测试时的全面性产生较大的提高。

作为一种形式化方法,其理论基础是形式语言,通过约束条件,可以将软件运行空间内的行为转化为可判定的数理逻辑问题,并通过形式化验证的方法加以检验。形式化验证的方法包括:定理证明、模型检测和等价性验证。

JML工具链

OpenJML

  • 包含Eclipse编辑插件、静态检查工具、运行时断言检查工具、反例浏览

JMLUnitNG & Sireum / Kiasan for Java & JMLUnit

  • 自动化测试样例生成工具

TACO & SMT Solver

  • 对Java代码与形式化表述的等价性进行验证

JMLUnitNG 测试数据

输入指令:

java -jar test\jmlunitng.jar -v src\impl\MyGroup.java src\com\oocourse\spec3\main\Group.java src\com\oocourse\spec3\main\Person.java src\impl\MyPerson.java

MyGroup依赖的类也需要加入地址表中。

然后将jmlunitng.jar加入编译依赖,运行MyPerson_JML_Test.java。结果如下:

[TestNG] Running:
  Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Failed: <<impl.MyGroup@44e81672>>.addPerson(null)
Failed: <<impl.MyGroup@60215eee>>.addPerson(null)
Failed: <<impl.MyGroup@65e579dc>>.addPerson(null)
Failed: <<impl.MyGroup@61baa894>>.delPerson(null)
Failed: <<impl.MyGroup@b065c63>>.delPerson(null)
Failed: <<impl.MyGroup@768debd>>.delPerson(null)
Passed: <<impl.MyGroup@490d6c15>>.equals(null)
Passed: <<impl.MyGroup@7d4793a8>>.equals(null)
Passed: <<impl.MyGroup@449b2d27>>.equals(null)
Passed: <<impl.MyGroup@5479e3f>>.equals(java.lang.Object@27082746)
Passed: <<impl.MyGroup@66133adc>>.equals(java.lang.Object@7bfcd12c)
Passed: <<impl.MyGroup@42f30e0a>>.equals(java.lang.Object@24273305)
Passed: <<impl.MyGroup@5b1d2887>>.getAgeMean()
Passed: <<impl.MyGroup@46f5f779>>.getAgeMean()
Passed: <<impl.MyGroup@18e8568>>.getAgeMean()
Passed: <<impl.MyGroup@33e5ccce>>.getAgeVar()
Passed: <<impl.MyGroup@5a42bbf4>>.getAgeVar()
Passed: <<impl.MyGroup@270421f5>>.getAgeVar()
Passed: <<impl.MyGroup@52d455b8>>.getConflictSum()
Passed: <<impl.MyGroup@4f4a7090>>.getConflictSum()
Passed: <<impl.MyGroup@18ef96>>.getConflictSum()
Passed: <<impl.MyGroup@6956de9>>.getId()
Passed: <<impl.MyGroup@769c9116>>.getId()
Passed: <<impl.MyGroup@6aceb1a5>>.getId()
Passed: <<impl.MyGroup@ba4d54>>.getRelationSum()
Passed: <<impl.MyGroup@12bc6874>>.getRelationSum()
Passed: <<impl.MyGroup@de0a01f>>.getRelationSum()
Passed: <<impl.MyGroup@4c75cab9>>.getSize()
Passed: <<impl.MyGroup@1ef7fe8e>>.getSize()
Passed: <<impl.MyGroup@6f79caec>>.getSize()
Passed: <<impl.MyGroup@67117f44>>.getValueSum()
Passed: <<impl.MyGroup@5d3411d>>.getValueSum()
Passed: <<impl.MyGroup@2471cca7>>.getValueSum()
Failed: <<impl.MyGroup@5fe5c6f>>.hasPerson(null)
Failed: <<impl.MyGroup@6979e8cb>>.hasPerson(null)
Failed: <<impl.MyGroup@763d9750>>.hasPerson(null)
Passed: <<impl.MyGroup@5c0369c4>>.notifyPeopleRelated(null, null)
Passed: <<impl.MyGroup@2be94b0f>>.notifyPeopleRelated(null, null)
Passed: <<impl.MyGroup@d70c109>>.notifyPeopleRelated(null, null)

可以看到,JMLUnitNG对整型调用进行了测试,并对int边界数据进行了测试,但不支持对象的递归嵌套生成以完成测试。

因此,为方便测试,可以考虑使用建立纯基础数据类型的替代方法。

实际上实现一个支持对象递归嵌套的测试系统是十分困难的,如果出现循环依赖,便无法完成测试。

架构设计

这次主要是一个社交网络图论模型,架构较为简单。由MyPerson类负责管理Person节点数据,MyGroup类负责管理分组统计信息,MyNetwork类负责管理图论相关算法及算法缓存。

MyNetwork类:在关联连通性和连通块数量判定上采用了并查集算法,在点双连通判定上使用了剪枝后的Targan算法。

MyPerson类:数据管理,不负责算法实现。

MyGroup类:数据&统计信息管理。统计信息管理时采用了动态规划的方法。每次新增Person节点/新连边时,检索可能的关联边,更新关联统计数据。新增Person节点时,更新年龄统计数据。

特别的,Person节点相关数据存储时均使用节点id + HashMap进行索引,使得存取复杂度最高不超过O(log n)。

Bug分析

这次作业中测、强测、互测中均没有出现bug...

自测的过程中,第二次作业查看讨论区后发现有的地方按照实际功能理解,没有仔细看JML,导致出现了偏差。最后核对JML后修复了Bug。

第三次作业Targan算法一开始没有理解透彻,在大数据下出现了问题。仔细和网上资料、模板核对后修复了bug,主要是找到双联通分量后压栈的过程。

总结

To be honest... 确实觉得JML形式化方法还有很多不足,比如造成开发效率下降、理解效率下降。

在实际应用中,应将JML形式化方法、更抽象更易理解的数学语言描述、实际功能描述相结合,分别在工具链测试&验证、开发者形式化理解、产品与程序对接方面互相补充。

一百年前希尔伯特曾经有形式化证明一切数学定理的理想,虽然破灭了,但形式化验证程序从某种意义上是另一种继承,形式化一切程序似乎也可以构建一个数学上自洽的世界。

上一篇:OO第三单元总结


下一篇:面向对象第三单元总结博客