BUAAOO Unit3 JML形式化方法

2023-12-05 08:52:40

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形式化方法、更抽象更易理解的数学语言描述、实际功能描述相结合，分别在工具链测试&验证、开发者形式化理解、产品与程序对接方面互相补充。

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

码农公寓