梳理JML语言的理论基础、应用工具链情况
JML语言理论基础
JML（Java Modeling Language）是一种行为规范接口语言，通过使用不会被编译的注释形式，和固定关键字的语法，指定Java模块代码的行为。这些行为包括需要满足的前置条件、后置条件，和可能产生的副作用等。它贯彻了契约方法设计理念，通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具 以静态方式来检查代码实现对规格的满足情况。
JML的语法、关键字及其释义如下所示：
- JML以javadoc注释的方式来表示规格，有两种注释方式，行注释和块注释。其中行注释的表示方式 为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。
- @requires 子句定义该方法的前置条件
- @assignment 子句列出该方法可以修改的类成员属性
- @ensure 子句定义了该方法的后置条件
- @pure 子句表明该方法无副作用，即仅具有查询功能
- @constraint 子句定义了状态变化约束
- @invariant 子句定义了全过程中的不变式
- othing 关键词表明该方法对类成员属性不进行修改
- esult 关键词代表该方法的返回值
- forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
- exists表达式： 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
- sum表达式：返回给定范围内的表达式的和。
- product表达式：返回给定范围内的表达式的连乘结果。
- max表达式：返回给定范围内的表达式的最大值。
- min表达式：返回给定范围内的表达式的最小值。
- um_of表达式：返回指定变量中满足相应条件的取值个数。
JML的应用工具链：
- OpenJML：OpenJML可以对含有JML的代码进行编译 ，并提供不同类型的选项进行检查。-esc可以静态检查可能出现的隐藏bug，-rac是运行时检查，-check则可以检查代码是否符合JML规格要求。
- JMLUnitNG：可以根据代码中所写JML规范自动生成测试框架进行自动化测试。
构架设计分析
第一次作业
第一次作业主要是实现一个路径类Path和一个容器类PathContainer 。
第二次作业是在第一次作业的基础上实现数据结构类Graph，新增功能包括图的连通性和查找路径。
bug与修复
第一二次作业的bug主要是在添加重复的路径时，如分别在第一句和第三句添加 add path 1 2 3 / add path 1 2 3，我的作业会把其当成两条路径来记录，即id分别为1和2。
心得体会
这次作业给我留下了较为惨痛的教训，小bug不予以修改，会在之后的测试中很严重地影响到正确性。要防微杜渐。