(1)梳理JML语言的理论基础、应用工具链情况
概述:JML语言是一种为Java程序设计的规格语言,遵循契约式设计规则。
编译:规格是用Java注释的方式编写的,因此可以被任意Java编译器编译。
思想:JML继承了Eiffel,Larch和Refinement Calculus的思想,其目标是在保持可读性的同时,提供严格的形式语义。
作用:JML提供语义来严格描述Java模块的行为,防止模块设计者的设计错误。JML使用各种验证工具,例如运行时断言检查器和扩展静态检查器(ESC / Java),可帮助程序员进行开发。
语法:(略)需要注意的是,JML语言为了和代码本体区别开来,其语法和Java有较大不同。
工具链:基于JML的工具较为完善。Iowa State JML tools提供了断言检查编译器jmlc;jmldoc可以生成含有额外JML信息的Javadoc;jmlunit根据JML生成单元测试。此外还有ESC/Java2(拓展的静态检查工具)、OpenJML(ESC/Java2的继承者)等等。
(2)【改为选做,能较为完善地完成的将酌情加分】部署SMT Solver,至少选择3个主要方法来尝试进行验证,报告结果,有可能要补充JML规格
(3)部署JMLUnitNG / JMLUnit,针对Graph接口的实现自动生成测试用例(简单方法即可,如果依然存在困难的话尽力而为即可,具体见更新通告帖), 并结合规格对生成的测试用例和数据进行简要分析
首先手写一个Test.java用于测试:
package test; public class Test { public Test() { } //@ public normal_behavior //@ requires (((long)i + (long)j) <= Integer.MAX_VALUE && (long)i + (long)j >= Integer.MIN_VALUE); //@ ensures esult == (i + j); //@ public exceptional_behavior //@ requires !(((long)i + (long)j) <= Integer.MAX_VALUE && (long)i + (long)j >= Integer.MIN_VALUE); //@ signals (IllegalArgumentException e) true; public int sum(int i, int j) throws RuntimeException { if ((long)i + (long)j <= Integer.MAX_VALUE && (long)i + (long)j >= Integer.MIN_VALUE) { return i + j; } throw new IllegalArgumentException(); } public static void main(String[] args) { } }
初始文件结构:
├── test
│├── Test.java
Step 1.
java -jar jmlunitng.jar test/Test.java
Step 2.
javac -cp jmlunitng.jar test/*.java
Step 3.
java -jar openjml.jar -rac test/Test.java
Step Final.
java -cp jmlunitng.jar test.Test_JML_Test
Execution Result:
[TestNG] Running: Command line suite Failed: racEnabled() Passed: constructor Test() Passed: static main(null) Passed: static main({}) Passed: <<test.Test@6c629d6e>>.sum(-2147483648, -2147483648) Passed: <<test.Test@5ecddf8f>>.sum(0, -2147483648) Passed: <<test.Test@3f102e87>>.sum(2147483647, -2147483648) Passed: <<test.Test@6fdb1f78>>.sum(-2147483648, 0) Passed: <<test.Test@51016012>>.sum(0, 0) Passed: <<test.Test@29444d75>>.sum(2147483647, 0) Passed: <<test.Test@2280cdac>>.sum(-2147483648, 2147483647) Passed: <<test.Test@1517365b>>.sum(0, 2147483647) Passed: <<test.Test@4fccd51b>>.sum(2147483647, 2147483647) =============================================== Command line suite Total tests run: 13, Failures: 1, Skips: 0 ===============================================
PS:racEnabled Failed的问题暂未找到方法解决:(。
在自动生成的测试中,对多种特殊情况都进行了测试。0、-2147483648、2147483647三个值互相加减,来测试是否符合jml要求。可见,jml不仅用于辅助设计,还可用于验证代码正确性。
(4)按照作业梳理自己的架构设计,并特别分析迭代中对架构的重构
首先生成类图:
两根蓝线清晰表明:三次作业,MyGraph继承MyPathContainer,MyRailSystem继承MyGraph。这样基于上次作业的正确性,避免机械的copy,最大限度保持程序的可维护性,呈现出清晰的数据结构。对于特殊的数据,建立独立类,单独维护。当然,继承不等于纯继承。为了添加新的功能,有必要维护旧的架构。例如:第二次作业MyGraph类需要实现求最小路径等。如何在继承的前提下实现新功能呢?我的解决方案是在MyPathContainer类的 addPath 方法中添加新的 addInGraph 方法,并在MyPathContainer中声明此方法,其内容为空。
public void addInGraph(Path p) { }
在MyGraph中对方法进行重载。
public void addInGraph(Path p) { for (int i = 0; i < p.size() - 1; i++) { int a = p.getNode(i); int b = p.getNode(i + 1); mirrorAdd(a); mirrorAdd(b); a = getMirrorId(a); b = getMirrorId(b); edgeMat[Math.min(a, b)][Math.max(a, b)]++; } linJieMat = genWholeLinJie(); minDisMat = floyd(genWholeLinJie()); addInSystem(p); }
(5)按照作业分析代码实现的bug和修复情况
在三次强测与互测中无bug。