OO第三单元总结
时间:2020-05-23 20:25:38
收藏:0
阅读:59
JML语言的理论基础、应用工具链
JML语言
JML是一种面向JAVA,形式化的行为接口规格语言。
JML表达式
-
原子表达式
\result
:方法执行后的返回值
\old(expr)
:一个表达式expr
在相应方法执行前的取值
\not_assigned(x,y)
:返回true
表示括号中的变量在方法执行过程中没有被赋值,false
则表示被赋值
\not_modified(x,y)
:限制括号中的变量在方法执行期间取值不发生变化 -
量化表达式
\forall
:全称量词修饰的表达式
\exists
:存在量词修饰的表达式
\sum
:返回给定范围内的表达式的和
\max
:返回给定范围内表达式的最大值
\min
:返回给定范围内表达式的最小值 -
集合表达式
实验和作业中还未应用到 -
操作符
\nothing
:表示空集
\everything
:表示全集
方法规格
- 前置条件
requires P
:表示调用者确保P为真 - 后置条件
ensure P
:表示方法实现者确保执行返回后,确保P为真 - 副作用范围限定
assignable
或modifiable
:限定方法执行过程中修改对象的范围 - 异常
signals
:抛出异常
类型规格
- 不变式
invariant
:要求所有可见状态下都必须满足的特性 - 状态变化约束
constraint
:对前序可见状态和当前可见状态的关系进行约束
工具链
- OpenJML:检查JML语法的正确性
- JMLUnitNG:自动化单元测试生成工具
架构设计
第一次作业
- 第一次作业较为简单,理解了JML规格后基本不需要花太大功夫就能完成
第二次作业
- 较第一次作业,JML复杂度提升,Person类变化不大,增加Group类,NetWork类稍有变化。不同于第一次作业,需要在算法上多做考虑。基础测试非常弱,自己也没有进行完整的测试,导致强测损失惨重。
第三次作业
- 较第二次作业,Person类依旧基本不变,Group类增加删除功能,NetWork增加大量查询方法,稍不注意就会写出Bug或是超时。
我牺牲了空间来换取时间,在Person类,Group类中使用ArrayList存person,HashMap存(id,listIndex)对,利用HashMap查询迅速的特性,稍稍降低查询时间。
第二次作业中,找通路我使用了bfs的方法,并在第三次作业一开始,直接沿用到新增的方法中,但是对规格理解错误,导致产生bug。后来通过评论区交流贴,吸取大家经验,使用dijkstra来查询最短路径。
代码Bug
第三次作业中,在阅读最短路径的JML时,理解错误,没有用到边的权值,直接想当然把结点数作为路径长度,测试做得也不全面,导致强测出现bug。
在设计新增的几个方法时,没有想到好的方法,直接跟着JML写,出现了超时。目前正在bug修复。
心得体会
JML的出现大大方便了程序设计中,程序员对于需求的提取,一个优秀的规格能给我们提供很多便利。
同时,也更注重程序的复杂度,设计的时候,保证正确性的情况下,多对算法进行考虑。
评论(0)