标签：成熟 hang sed ddc ever 引入 中间 cto lun
在面向对象课程中的第三章，我尝试了基于JML语言的规格化设计，按照AppRunner中的接口文件实现了Path类和PathContainer, Graph, RailWaySystem迭代类。JML语言是一种规格化语言，完全建立于数理逻辑上，既能够为开发者实现类与方法时提供准确的功能参考，也能够在特定工具支持下充当assert的功能和辅助自动生成测试样例。
本篇博客将从以下几方面对第三章进行总结：
常用原子表达式
\result
\old(expr)
\assignable
\nonnullelements
\not_assigned(x,y,...) \not_modified(x,y,...)常用量化表达式
\forall \\ 给定元素；前提范围；后置约束（张三 在学校里面 一定不玩游戏）
\exist \\ 给定元素；前提范围；后置约束
\sum \\ 给定元素；前提背景；累加对象
\product \\ 给定元素；前提背景；累乘对象
\max \min \num_of常用集合表达式
new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() } 操作符
A <: B \\ A是B的子类时为真
A <==> B ; A <=!=> B \\ 与==和！=相同效果，但优先级更低
A ==> B \\ 推理
\nothing; \everything \\ 空集；当下作用域能够访问的所有变量。
\\常用assignable \nothing来表示pure类方法类型规格
在尝试编写JML规格和根据JML规格填充代码时，主要使用了VS-Code、OpenJML和JMLUnitNg，在本部分我将主要介绍前面两者，最后者放在第2章节具体介绍。
VS-Code
VS-Code主要提供了Java+Jml的语法插件支持，从而对注释中的JML语言进行了高亮，便于在撰写规格时的语法检查和实现规格时的阅读清晰。
OpenJML
根据OpenJML相关文档，OpenJML提供三种类型的检查：
形式化检查（Type Checking）：
3 + True运算不匹配等各类问题，属于静态检查——Static Checking的一部分。\result、不符合类型的赋值和比较等……java -jar openjml.jar Student.java
- The resulting AST may then be subjected to various checks to ensure that certain obvious errors are avoided (static analysis).One common form of static analysis is type-checking.
- After this, the AST will be fed to an evaluator or interpreter to execute the program—or else to a compiler to translate it into executable low-level code.
- https://www.inf.ed.ac.uk/teaching/courses/inf2a/slides2017/inf2a_L14_slides.pdf
静态检查（Static Checking）：
静态检查是根据撰写的JML规格，检测实现的方法和类中是否有与规格定义相违背的地方，在这里似乎有多种Solver可以配置使用，以实现不同的检查。
执行命令：java -jar openjml.jar -esc -exec Solvers-windows/z3-4.7.1.exe B.java，这里遇到了奇怪的问题，如果不使用-exec指定相应的证明器，则不能运行成功，并且三个证明器也仅有z3-4.7.1的版本能够运行成功，目前猜测可能是遇到了windows版本的运行环境的问题。
public class B {
static /*@ spec_public*/ int j,k;
//@ requires i >= 0;
//@ modifies j;
//@ ensures j == i;
public static void setj(int i) {
k = i;
return;
}
//@ ensures j == 1;
public static void main(String[] args) {
setj(3);
return;
}
}
B.java:16: 警告: The prover cannot establish an assertion (Postcondition: B.java:13: 注: ) in method main
return;
^
B.java:13: 警告: Associated declaration: B.java:16: 注:
//@ ensures j == 1;
^
B.java:10: 警告: The prover cannot establish an assertion (Postcondition: B.java:7: 注: ) in method setj
return;
^
B.java:7: 警告: Associated declaration: B.java:10: 注:
//@ ensures j == i;
^
B.java:9: 警告: The prover cannot establish an assertion (Assignable: B.java:6: 注: ) in method setj: k
k = i;
^
B.java:6: 警告: Associated declaration: B.java:9: 注:
//@ modifies j;
^运行时检查（Runtime Assertion Checking）：
assert语句检查类和方法在运行过程中是否符合规定。java -jar openjml.jar -rac Student.java + java -classpath ",;jmlruntime.jar" Student我使用了课程组JML教程中的Student类中的addCredits方法进行尝试，方法要求传入的变量为非负整数，我调用此方法并输入负数时，程序就出现了错误信息，从而帮助我定位错误： /*@ requires c >= 0;
@ ensures credits == \old(credits) + c;
@ assignable credits, master;
@ ensures (credits > 180) ==> master;
@*/
public void addCredits(int c) {
updateCredits(c);
if (credits >= 180) {
changeToMaster();
}
}
此部分的内容十分感谢伦泽标同学对JMLUnitNG自动测试工具的探索与分享，在这里我使用课程组JML教程中的Student类作为被测试对象，记录相关的测试指令，浅析自动测试的相关特点。
我在运行自动测试时脚本如下：
java -jar jmlunitng.jar student/Student.java # 生成自动测试源码
javac -cp jmlunitng.jar student/*.java # 编译自动测试源码
java -jar ../openjml.jar -rac student/Student.java # 编译源文件为rac，用于运行时检测
echo "begin to check"
java -cp jmlunitng.jar student.Student_JML_Test # 启动自动测试
pause[TestNG] Running:
Command line suite
Passed: racEnabled()
Failed: constructor Student(null)
Passed: constructor Student()
Skipped: <<student.Student@574caa3f>>.addCredits(-2147483648)
Passed: <<student.Student@6c629d6e>>.addCredits(0)
Passed: <<student.Student@5ecddf8f>>.addCredits(2147483647)
Passed: <<student.Student@3f102e87>>.getName()
Failed: <<student.Student@27abe2cd>>.setName(null)
Passed: <<student.Student@6fdb1f78>>.setName()
===============================================
Command line suite
Total tests run: 9, Failures: 2, Skips: 1
===============================================第一次作业
第一次作业的类划分比较简单，除实现的两个接口类以外，额外引入了DoubleDirMap类基于HashMap双向映射Path和PathId，而也正是因为将功能划分地很细致和明确，作业一的代码复用率几乎以100%复用。由于基本上都是实现的接口方法，自定义方法很少，因此不再进行量化分析。
第二次作业和第三次作业
虽然有接口类指导顶层类的设计，但是内部功能的实现与性能优化则需要自行设计，本章作业中，我高兴地发现自己在Graph中所实现了架构在RailWayStation中竟然有许多的复用情况，这一点也确实说明在经过OO课程的洗礼后，对程序的功能架构有了一定的提升。
由于作业二与作业三一脉相承，在此我将主要展示第三次作业中的架构。
─subway
│ MyRailwaySystem.java
│
├─algorithm
│ │ InfectGraph.java
│ │
│ └─shortest
│ LeastTransfer.java
│ LeastUnpleasant.java
│ LowestTicketPrice.java
│ ShortestPath.java
│ ShortestPathModel.java
│
├─component
│ │ DoubleDirPathMap.java
│ │ MyPath.java
│ │
│ ├─link
│ │ Link.java
│ │ LinkContainer.java
│ │
│ └─node
│ NodeCountMap.java
│
└─tool
AlgorithmFactory.java
Constant.java
ConvertMap.java
Matrix.java
VersionMark.java在图论的问题里，图的结构和运行在图上的算法基本可以完全所有类型的图问题，因此，我的类采用结构+算法的构造，结构随着每一次路径的增删实现实时的更新，算法则内部根据缓存版本和图当前的结构类，实现相应功能。
结构类：与结构有关的类都被定义在component包内。MyPath是路径类；DoubleDirPathMap用于维护路径类与路径ID之间的关系；Link和Node是对加入图的Path具体拆分和解析后形成的相关类，分别用于维护图结构两个基本的要素——点和边的详细信息（例如点全集、某点所在的路径编号、某点所连的边、某点所连边的路径编号……），正是这些详细信息使得图上的算法成为可能。
算法类：与算法相关的类都被定义在algorithm包内。
InfectGraph用于统计连通块的数量，此功能和其他功能实现算法不同，采用的是BFS+染色的方式。shortest包中包含了4种跑在不同边权图上的最短路算法，我采用的是拆点建图+最短路SPFA的方式求解此问题：将真实点拆成虚拟点，使每个虚拟点只对应一个真实点且只对应真实点所在的一条路径，探讨对应相同真实点的虚拟点间的边权，从而解决换乘成本问题。由于只是新图上的边权有4种不同的定义，因此需要重写的就只有边权的赋值方法，为此我定义了ShortestPathModel抽象类实现除边权赋值外的所有方法，并定义getEdgeValue抽象方法以要求所有的继承类必须要实现该方法。A = 虚拟点所对应的物理点相同
B = 虚拟点所对应的路径相同
| A=True B=True | A=True B=False | A=False B=True | A=False B=True | |
|---|---|---|---|---|
| 最短路 | 0 | 0 | 1 | - |
| 最小换乘 | 0 | 1 | 0 | - |
| 最低票价 | 0 | 2 | 1 | - |
| 0 | 32 | $H(e_1,e_2)$ | - |
工具类：工具类的定义，旨在减少类和方法中声明过多成员变量的问题。
复杂度分析
根据量化指标，整个工程的复杂度还是不错的，部分类出现OCavg指标过高的主要原因是if-elseif-else条件判断分支过多，集中在抛出异常和工程模式中。
而分析了类依赖性的量化指标和依赖矩阵，说明程序对类功能划分设计得是合理的，都没有体现出过高的依赖性.
在本章的三次作业中，受益架构划分得比较清晰和针对每个方法的单元测试，在强测和互测阶段都没有出现Bug，而对于其他同学的Bug，我在阅读代码中发现的Bug如下：
经过对一些简单的JML规格填充，我对其撰写有以下三点感悟：
在我看来，JML语言不同于Javadoc等自然语言注释，其本身就是由纯数理逻辑所形成的，这样的规格优点是无二义性、在一定工具的支持下能够配合自动化检查。但是缺陷则是随着方法的需求变得复杂和感性，需要花费大篇幅的JML规格去阐释从人的角度很容易理解的内容，就像第三次作业中换乘条件的加入引入了大量无需程序员实现的pure方法，而且规格也容易出现很多的错误，并且由于这些方法并不需要实现，JML规格的自动检查功能实际已经丧失了。
因此，JML的应用情景我认为还是需要进一步商榷和深究的，目前认为用在系统体系结构、数论、图论等逻辑数理性强的领域更为适合，并且甚至还可能借助于已经成熟的机器证明体系以实现JML自动化生成；而对于一些实际生活应用的例子，则可以通过自然语言注释+黑/白名单特例的形式进行阐述。
标签：成熟 hang sed ddc ever 引入 中间 cto lun
原文地址：https://www.cnblogs.com/sinoyou/p/10908763.html
