【面向对象】第三单元总结——JML

梳理JML语言的理论基础、应用工具链状况

JML语言理论基础

JML（Java Modeling Language）是一种行为规范接口语言，经过使用不会被编译的注释形式，和固定关键字的语法，指定Java模块代码的行为。这些行为包括须要知足的前置条件、后置条件，和可能产生的反作用等。它贯彻了契约方法设计理念，经过JML及其支持工具，不只能够基于规格自动构造测试用例，并整合了SMT Solver等工具 以静态方式来检查代码实现对规格的知足状况。

JML的语法、关键字及其释义以下所示：

• JML以javadoc注释的方式来表示规格，有两种注释方式，行注释和块注释。其中行注释的表示方式 为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。
• @requires 子句定义该方法的前置条件
• @assignment 子句列出该方法能够修改的类成员属性
• @ensure 子句定义了该方法的后置条件
• @pure 子句代表该方法无反作用，即仅具备查询功能
• @constraint 子句定义了状态变化约束
• @invariant 子句定义了全过程当中的不变式
• \nothing 关键词代表该方法对类成员属性不进行修改
• \result 关键词表明该方法的返回值
• \forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每一个元素都知足相应的约束。
• \exists表达式： 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素知足相应的约束。
• \sum表达式：返回给定范围内的表达式的和。
• \product表达式：返回给定范围内的表达式的连乘结果。
• \max表达式：返回给定范围内的表达式的最大值。
• \min表达式：返回给定范围内的表达式的最小值。
• \num_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不予以修改，会在以后的测试中很严重地影响到正确性。要防微杜渐。