JML是一种形式化的、面向java的行为接口规格语言。可用于指定Java模块的行为 。它结合了Eiffel的契约方法设计 和Larch 系列接口规范语言的基于模型的规范方法 ,以及 细化演算的一些元素 。
比较常用的JML工具链是Openjml,jmlunitng等
-
主要由三部分构成对方法的描述:前置条件,后置条件,副作用
-
主要语法如下:
-
/@ requires P; @
-
/@ ensures P; @/ Postcondition
-
/@ assignable list;@/ Side-Effects
-
/@ signal (Exception e) P;@/ Exception
-
/@ invariant P; @/ Invariant不变式
-
/@ constraint P; @/ Constraint 限制
-
\result method result reference
-
\old(E)Previous expression value
-
Openjml常用命令:
-
openjml -check demo1.java
-
openjml -check *.java
-
静态检查:openjml -esc <source files>
-
运行时检查: openjml -rac <source file>,会生成相应的assertion
实测结果:
测试用例时最简单的加减,原来尝试了自己作业中的方法,但是命令行编译的时候总是有一点错误,所以还是转向了伦泽标大佬的程序。我认为重要的是理解Jml是怎么运作的,下面给出我对JML的认识:
-
前置条件和后置条件使得这个方法的正确性得到验证
-
判断边界条件
-
多组数据测试
这是我的测试程序生成的文件,可以看到主要对整数,包结构,和string进行了测试,在data文件夹中,是这样的组织形式:
可以看到,主要是对功能进行了封装与测试
架构设计分析
第一次作业:
第一次作业的目的是实现一个路径管理器,主要实现以下功能:
-
添加路径
-
删除路径
-
查询路径id
-
根据id获取路径
-
获取容器内路径总数
-
根据路径id获得大小
-
获得路径节点数
-
根据节点序列/id判断容器是否包含
-
容器节点数
-
比较路径
-
路径是否包含某节点
关系到性能和正确性的几乎都在pathcontainer类上,因此这里只分析这个类
-
由于需要id 节点序列双向查询path,因此需要一个hashmap<id, path>,虽然这样根据path查询会非常低效。但是不至于时间爆炸。
-
对路径中节点的包含和查询情况,为了节省时间,使用了冗余的hashset存储路境内节点。
-
比较路径只需调用实现好的接口compareable即可
-
比较难的,便是这个容器内的总结点数。最初没有考虑很多,才使用了迭代器的方式挨个计算。但是强测结果不尽人意。采取保留中间结果和冗余数据存储的方式可以大大降低时间复杂度。Bug修复的时候add和remove维护了多余的nodelist便解决了错误。
第二次作业:
这次作业的目的是实现图管理,相比上次有一点点难度增加,但是依然比较简单。主要增加的功能是:
-
容器是否存在一条边
-
两个节点是否连通
-
两节点最短路径
这次作业必须在每次更新图结构的时候重新维护所有数据结构,否则无法判断某条边是不是真的连通。在讨论区的启发下,我引入了floyd矩阵,一下解决三个问题,并且时间性能也非常好。
这次作业重构在以下方面:
-
大胆增加add, remove复杂度,每次改变图结构都重新计算。
-
重写了hash方法,上次作业并没有考虑hashcode的问题,在同学的启发下,发现时间复杂度高很可能是将大部分PATH都映射在同一个位置上,这次进行重构后性能大大提升。
第三次作业:
是祸是福,我没写出来,但是我还是很认真的看了大佬的代码以及网上的博客
这次是在前两次作业的基础上实现地铁管理,其实就是实现两个有权重的矩阵最短路径,该矩阵需要考虑节点是否在同一条路径上。另外就是连通块数量,可以通过并查集实现。
这次作业新增的需求:
-
连通块数量
-
最低票价
-
最低不满意
-
最少换乘
怎么实现才可以:
-
并查集实现连通块数量统计:
-
维护一个树结构,初始时是所有元素
-
遍历所有的边,如果两个点连接在一起,就将这两个点对应树的根节点合并在一起。原则是,小树挂在大树上,并且这两棵树的根节点尽可能只隔一代。
-
-
关于换乘导致的最短路径问题:原来只需要在同一个图中的两点权值加上固定值,最后再减掉就好了。
我为什么又挂了:
-
我也很难受啊 -
自作聪明地以为如果刷新前foyld两点没有联通,并且这次可以将他们连通就说明他们没有在同一条路径上。这在小数据集上得到多次证实,但是大数据集一定会挂。我的想法:
-
添加一条新路径首先打通这条路径内部,并不更新它和其他路径,复杂度为这条路的节点数
-
接下来通过判断上次是不是两节点不连通来确定他们是不是不连通,更新最低票价和最低不满意。
-
连通块单独维护一个数据结构,使用了链表(我没有看过讨论区),时间复杂度为O(节点数N)
-
-
太浮躁了,没有利用好时间,对上次架构太自信,不听取别人的意见,没有好好交流,不够重视,赶DDL,下次的重头戏,我肯定可以写出来
-
在想出一个比较创新的方法的时候,一定要对其正确性进行推演,否则一定会翻车的
关于规格撰写:
这几次的作业明显是在教我们从需求出发设计每个类的实现和规格。个人不是很喜欢这种风格的说明文档。因为JML要求太严格了,撰写JML的成本比较高,需要熟练掌握它的语法,甚至还要de它的Bug,但不得不说,单元测试是一个比较好的习惯,我很希望自己下一次作业工程量变大的时候可以尝试一下单元测试,全方位保证自己的正确性。