OO第三单元--JML规格

JML理论基础

JML是用于对Java程序进行规格化设计的一种表示语言。与自然语言会带来的歧义性不同，JML语言通常都具有独一的意义，因此，常被用来实现逻辑严密的规格。

注释结构

JML的注释方法一般有两种：

• 行注释：//@annotation
• 块注释：/* @ annotation @ */

JML表达式

• 原子表达式
  • \result表达式：表示方法执行后的返回值
  • \old(expr)表达式：表示一个表达式expr在相应方法执行前的取值
  • \not_assigned(x,y,······)表达式：用来表示括号中的变量是否在方法执行过程中被赋值
  • \not_modified(x,y,······)表达式：用来表示括号中的变量在方法执行期间的取值未发生变化
  • \nonnullelements(container)表达式：表示container对象中存储的对象不会有null
  • \type(type)表达式：返回类型type对应的类型
  • \typeof(expr)表达式：该表达式返回expr对应的准确类型
• 量化表达式
  • \forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束
  • \exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束
  • \sum表达式：返回给定范围内的表达式的和。
  • \product表达式：返回给定范围内的表达式的连乘结果
  • \max表达式：返回给定范围内的表达式的最大值
  • \min表达式：返回给定范围内的表达式的最小值
  • \num_of表达式：返回指定变量中满足相应条件的取值个数
• 集合表达式
  • 一般形式为：new ST {T x | R(x)&&P(x) }
  • R(x)对应集合中x的范围，通常是来自于某个既有集合中的元素
  • P(x)对应x取值的约束
• 操作符
  • 子类关系操作符：E1<:E2,如果E1是类型E2的子类型，则该表达式的结果为真，否则为假
  • 等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2，其中b_expr1和b_expr2都是布尔表达式
  • 推理表达式：b_expr1==>b_expr2或者b_expr2<==b_expr1
  • 变量引用操作符
    • \nothing指示一个空集
    • \everything指示一个全集

方法规格

JML对于方法的规格主要有三个部分

• 前置条件(pre-condition)：前置条件一般通过requires子句来表示
• 后置条件(post-condition)：后置条件一般通过ensures子句来表示
• 副作用范围限定(side-effects)：副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据

类型规格

类型规格值对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所涉及的约束规则。

我们主要会涉及两类，不变式限制(invariant)和约束限制(constraints)

• 不变式invariant:不变式是要求在所有可见状态下都必须满足的特性。其中可见状态包括以下几种
  • 对象的有状态构造方法的执行结束时刻
  • 在调用一个对象回收方法来释放相关资源开始的时刻
  • 在调用对象o的非静态、有状态方法的开始和结束时刻
  • 在调用对象o对于的类或父类的静态、有状态方法的开始和结束时刻
  • 在未处于对象o的构造方法、回收方法、非静态方法被调用过程中的任意时刻
  • 在未处于对象o对于类或者父类的静态方法被调用过程中的任意时刻
• 状态变化约束constraint：constraint一般用来对前序可见状态和当前可见状态的关系进行约束

JMLUnitNG

[TestNG] Running:
Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Passed: <<MyGroup@1ab7767>>.addPerson(null)
Passed: <<MyGroup@722c82d8>>.addPerson(null)
Failed: <<MyGroup@98ba811c>>.addRelation(-2147483648)
Failed: <<MyGroup@4ee0c29a>>.addRelation(2147483647)
Passed: <<MyGroup@6124fbb2>>.addRelation(0)
Failed: <<MyGroup@77db4eae>>.addRelation(2147483647)
Passed: <<MyGroup@d0a988d5>>.delPerson(null)
Passed: <<MyGroup@13399d24>>.delPerson(null)
Passed: <<MyGroup@1510e06>>.equals(null)
Passed: <<MyGroup@e3414c71>>.equals(null)

===============================================
Command line suite
Total tests run: 14, Failures: 5, Skips: 0

===============================================

Process finished with exit code 0

可以看出，测试主要是针对于传入参数为null和INT_MAX、INT_MIN这类比较边界的条件，错误的情况也主要是对于边界条件的处理上。这个也是我在考虑代码时所没有考虑到溢出的情况而导致的。

架构设计

本次架构设计主要针对于最后一次拓展情况进行分析，最后一次设计类图如下

本次架构基本上是按照MyPerson、MyNetwork、MyGroup实现的，只是引入了一个Tuple类用于实现类似python语言中元组的功能。从整体架构上来讲MyNetwork类相对显得有些许臃肿。在作业结束后反思我认为还是应该以迭代的设计方法来实现这三次作业。比如第二次作业就可以在第一次的基础上实现继承，并对MyNetwork类实现Group相关方法的实现。第三次作业可以在第二次作业的基础上实现继承，并添加相应的图算法。

BUG情况

对于本单元而言，因为过于信赖中测的原因，BUG存在相对还是较多的。

第一次作业：强测未能通过，主要BUG点在于isCircle方法中一个判断语句的错误，这个错误相对不是很起眼，但是如果进行了一定程度上的测试还是可以发现问题所在的。这也是我的问题所在。

第二次作业：强测仍然未能通过。由于上一次作业的惨痛教训，我对我的各类方法都进行了正确性的测试，然而万万没想到，我的莽夫实现方法(如每次在query相关属性的时候对集合进行遍历)导致了运行时间上的超时。

第三次作业：本次作业基本上是完全的重构，在容器选择上也采用了性能相对较高的HashSet和HashMap。同时对于一些经常访问的属性值也是进行了动态维护。同时也使用了较多的数据对本次各类方法进行测试。本次通过了强测测试，但本次因为对于集合初始化的原因，导致了部分测试点存在TLE的问题。

心得体会

本单元主要是基于JML规格开展的一系列代码实现。在头两次实现过程中，由于过度相信中测，导致了自己对代码测试不全，考虑不周的情况，同时也存在照着规格写代码的问题。其实本单元三次作业相对于前面两个单元的实现难度还是有一定程度上的降低的，但这一单元也用惨痛的教训来警示了我测试的重要性，任何时间都不能盲目地相信自己实现的代码。培养良好的代码测试习惯也是非常重要的一个能力。在后续的任务中我也会更为注重这一方面的问题。

OO第三单元--JML规格

原文：https://www.cnblogs.com/1806lay/p/12941790.html