// demo/Graph.java package demo; import java.util.ArrayList; public class Demo { /*@ public normal_behaviour @ ensures esult == lhs - rhs; */ public static int compare(int i, int j) { return i - j; } public static void main(String[] args) { compare(124, 376); } }
前言
Java 建模语言(Java Modeling Language, JML) 是一种用来进行详细设计的表示法，它倡导一种思考方法和类的新思路。
我们所学习的面向对象分析和设计的原则之一就是应当尽可能地将过程实现往后推，因此我们在进行编程时，会先从框架开始，完成类和方法的定义；当需要过程实现时，我们转向过程设想。设计架构时，我们应该将预期的功能记录下来以便实现方进行实现，注释是一种表达方式。但是，每个人的注释可能都不一样，自己的理解不一定符合他人的思路，这种“语言”隔阂无疑将架构和实现分离，造成信息不对称，从而影响作业效率甚至导致错误。而 JML 统一了注释的风格及含义，使得 JML 类型注释对所有人达意，帮助了我们完成设想与实现的无阻塞连接。
JML语言
理论基础
Java建模语言(JML)是一种行为接口规范语言，可用于指定Java模块的行为。它结合了Eiffel的契约式设计方法和Larch接口规范语言家族的基于模型的规范方法，以及一些细化演算的元素。
在使用方面，有以下规格：
-
注释结构：JML以javadoc注释的方式来表示规格，每行都以@起头
-
JML表达式: JML的表达式是对Java表达式的扩展，新增了一些操作符和原子表达式.
-
esult表达式：表示一个非void 类型的方法执行所获得的结果.
-
old( expr )表达式：用来表示一个表达式expr 在相应方法执行前的取值.
-
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束.
-
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
-
...
-
-
方法规格：方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。
-
前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为
真”。 -
后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执
行返回结果一定满足谓词P的要求，即确保P为真”。 -
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法规格的角度，必须要明确给出副作用范围。
-
工具链
Openjml ： OpenJML项目的目标是为JML和当前Java实现一个完整的工具，便于实践者和学生使用该工具指定和验证Java程序。
单元测试工具(JMLUnitNG) ： 一个用于jml注释的Java代码的自动化单元测试生成工具，包括使用Java 1.5+特性(如泛型、枚举类型和增强的for循环)的代码。与最初的JMLUnit一样，它使用JML断言作为测试预言。
JUnit--验证
按照讨论区帖子安装后，进行以下验证
准备阶段
生成前的文件树
demo
└── Demo.java
执行
1 jmlunitng demo/Demo.java
生成后的文件树
demo
├── Demo_InstanceStrategy.java
├── Demo.java
├── Demo_JML_Data
│ ├── ClassStrategy_int.java
│ ├── ClassStrategy_java_lang_String1DArray.java
│ ├── ClassStrategy_java_lang_String.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_String1DArray.java
└── PackageStrategy_java_lang_String.java
编译
-
用 javac 编译 JMLUnitNG 的生成文件
执行
javac -cp jmlunitng-1_4.jar demo/**/*.java -
用 jmlc 编译自己的文件，生成带有运行时检查的 class 文件
这一步直接使用 openjml 自带的 jmlc，执行
openjml -rac demo/Demo.java
测试
执行
java -cp jmlunitng-1_4.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 ===============================================
测试结果的第一行是 racEnabled 的测试，意在检测我们的主文件是否带有 JML 的运行时检查，若没有则跳过所有测试。
作业架构设计
.png?lastModify=1558529333)
第三次集合了第二次和第一次，不再赘述
代码实现的bug和修复情况
第一次作业
第一次作业没有什么难度，但是有一点还是值得注意的。
对于指令的输入，有以上几点限制。总上限3000条，PATH_ADD最多300条，每条路径最大节点数为1000，这意味着最多是300000个节点。此外，cpu时间限制为5s。一开始会被这次作业简单的外表迷惑，但是算下来要处理的数据挺多的，尤其是对于DISTINCT_NODE_COUNT，如果每次都要算一遍的话，一定会超时，因此在进行添加删除操作时需要计算该值，减少一次运行的压力。此外对于PATH，如果只采用list容器，对遍历操作有利，但是查询却是线性的，不利于PATH_CONTAINS_NODE类指令，因此考虑采用加入hash容器提高效率。
第二次作业
第二次作业在第一次作业的基础上增加了图的功能，增加了边、连通、路径等概念，对应CONTAINS_EDGE、IS_NODE_CONNECTED、SHORTEST_PATH_LENGTH。对于CONTAINS_EDGE，只需增加存储边的容器即可，采用hash容器，因为对edge主要涉及查询操作。对IS_NODE_CONNECTED指令，我采用了bfs（广度优先遍历）的方式计算；因为边没有权值，对于SHORTEST_PATH_LENGTH我也采用了bfs；
这次的数据限制如下：
bfs最佳复杂度接近O(n)，最差情况接近O(n^2)，在程序的最大运行cpu时间为20s的限制下，7000条bfs也是不太能够吃得消的。因此在这次的作业中我才用了缓存的机制——在进行bfs(i, i+n)时，我们实际上找到了 i 到达 i + 1、i + 2...等点的最短路径，因此可以使用容器存储这些可能用到的数据，以优化时间。当PATH_ADD/PATH_REMOVE的时候，需要注意以前的缓存已经失效，应设置版本更新机制。
第三次作业
第三次作业增加了Raiway的实现，即将第二次实验的图具现为地铁路线图，据此来得到LEAST_TICKET_PRICE、LEAST_TRANSFER_COUNT、LEAST_UNPLEASANT_VALUE等值，数据限制如下：
由于此次图的边有了TICKET_PRICE、TRANSFER_COUNT、UNPLEASANT_VALUE的值，所以这次问题抽象为为带权图之间的最短路径。此次作业我才用了dijkstra算法来查找最短路径。但由于个人的理解问题，导致没处理好换乘问题，没有通过中测。我本想着换乘可由上一条路径和下一条路径确定，比如1-2-4，2-3-5，那么1-5的历程为1-2-3-5。由我的算法，1-2-3为换乘因为1-2在PATH1上，2-3在PATH2上。但是我忽略了1-2-3，2-3-4，从1到4，历程1-2-3-4的情况，根据我的算法是没有换乘的，因此导致了这次作业的失败，我没有意识到地铁站的id即便相同，其换乘的含义也不一定是一样的。修复时采用了讨论区dalao的拆点的算法，将地铁站的换乘意义分开了。
对规格心得体会
这单元我们面向对象的课程主要讲了关于规格的一些内容。一开始我对java的规格并不是很理解，感觉对于程序可以写规格，但是没必要。不是说没必要写架构类注释，而是规格本身并不容易写，因为这两次作业的规格甚至比实现的代码还多、比源码还难以理解，给我一种还不如用伪代码来写。但是现在通过这单元的学习，我对规格有了更进一步的了解——还是不理解为什么要写，可能是境界还未达到。希望自己以后学习更多的知识，开阔自己的视野，继续努力！