欢迎您访问程序员文章站本站旨在为大家提供分享程序员计算机编程知识!
您现在的位置是: 首页  >  IT编程

OO第三单元总结——JML

程序员文章站 2022-04-09 09:28:49
目录 写在前面 JML理论基础 JML工具链 JMLUnitNG的使用 架构设计 Bug分析 心得体会 写在前面 OO的第三单元学习结束了,本单元我们学习了如何使用JML语言来对我们的程序进行规格化设计。并对openjml以及JMLUnitNG、JUnit等工具的使用有了初步的了解。 JML理论基础 ......

目录

  • 写在前面
  • jml理论基础
  • jml工具链
  • jmlunitng的使用
  • 架构设计
  • bug分析
  • 心得体会

写在前面

oo的第三单元学习结束了,本单元我们学习了如何使用jml语言来对我们的程序进行规格化设计。并对openjml以及jmlunitng、junit等工具的使用有了初步的了解。

jml理论基础

注释结构

jml以javadoc注释的方式来表示规格,每行都以@起头。

jml表达式

jml表达式有一下几种:

  • 原子表达式:如\result\old等。
  • 量化表达式:如\forall\exists等。
  • 集合表达式:这个不怎么常用,比如new jmlobjectset {integer i | s.contains(i) && 0 < i.intvalue()}
  • 操作符:常用的包括等价关系<==>,推理关系==>,变量引用\nothing等。

jml方法规格

  • 前置条件:通过\requires p表示,是对方法调用者的要求,意思是调用者确保p为真。
  • 后置条件:通过\ensures p表示,是对方法实现者的要求,意思是方法实现者确保方法执行返回结果一定满足谓词p的要求,即确保p为真。
  • 副作用范围限定:通过\assignable x表示,其中x为此方法可以更改的对象,极端情况为\nothing\everything
  • signals子句:一般用来限制抛出异常的条件。

jml类型规格

  • 不变式invariant:是要求方法在所有可见状态下都必须满足的特性。
  • 状态变化约束constraint:是要求对象的状态在变化时也要满足的约束。

jml工具链

  • 使用openjml对实现的代码进行检查:包括jml语法静态检查,代码静态检查,运行时检查。
  • 使用jmlunitng根据jml语言自动生成testng测试。

jmlunitng的使用

针对如图的compare方法,利用jmlunitng生成测试样例:

OO第三单元总结——JML

生成的样例点:

OO第三单元总结——JML

可以看到,自动生成的样例点对方法的各种边界情况进行了测试,包括正数和正数,正数和负数,负数和负数,还有0的情况,如果我们写的方法出现了加减法溢出的问题,这些测试样例也都会检测出来并报failed。

架构设计

第九次作业

本次作业主要内容是实现path和pathcontainer,其中主要的查询方法是不同节点数的个数,我使用了均摊策略,即把查询的时间复杂度平均到addpath和removepath中,每次添加或删除路径时更近存放节点的hashmap,这样可以实现o(1)复杂度的查询方法。

第十次作业

本次作业是实现path和gragh,而gragh是继承了pathcontainer的,所以我在写的时候也使用了继承。本次作业的主要查询方法是最短路径,所以我重写了pathcontainer里面的addpath和removepath方法,在添加删除路径的时候重新建图,并更新最短路径。对于pathcontainer里面的其他方法,直接继承使用。

本次作业我使用的方法:

  • floyd多源最短路算法
  • hashmap嵌套实现邻接矩阵的存储

第十一次作业

本次作业是实现path和raiwaysystem,其中railwaysystem继承了gragh。本次作业涉及到加权图以及换乘的代价,所以算法难度较大。在拓展的时候,我还是重写了addpath和removepath方法,并添加了几个方法来计算新的最短路问题。

本次作业我使用的方法:

  • 分层的floyd算法:即图结构变更之后,先对每条路径内部的点使用floyd算法更新最短路,然后加上换乘代价,再对所有路径中的所有节点使用folyd算法,即可实现带换乘代价的最短路算法。
  • 静态数组存储结构:即用二维静态数组替代hashmap嵌套来实现邻接矩阵的存储,这样做的优点是计算速度,存取速度快,减少时间复杂度。缺点是不好维护和拓展。如果不是追求极致性能,还是慎用此类方法。
  • 计算连通块的数量:使用并查集。

bug分析

第九次作业

本次作业中,我的bug是减法溢出,具体是因为:我在实现compareto方法的时候,采用的是两个整数相减来判断大小。而如果出现减法溢出的情况,那么判断结果跟正确答案是正好相反的。为此我也炸了强测+互测的20多个点。

本次作业中,同组同学的bug有:查询方法复杂度过高从而导致tle,还有跟我一样的减法溢出问题。

第十次作业

本次作业中我的程序未被发现bug,我也未发现其他同学的bug

第十一次作业

本次作业中我的程序也未被发现bug,我也未发现其他同学的bug

心得体会

规格撰写方面

本单元让我体会到真正参与编写一个工程的感觉,即在一整个工程中分出一小部分让我们完成,并且要符合工程的要求。在这种情况下,jml语言体现出非常大的作用,它非常方便,不关注方法的实现过程,只专注于前因后果,因为只有前因后果才是把整个工程的思路贯穿起来的渠道。

此外,我也尝试过自己根据已有方法编写jml,也是有很大难度的,一定程度上,比我们写代码要难得多,这也体现出来规格化的重要性。

junit初体验

针对本单元各种小型模块的测试,我第一次使用了junit这个工具。可以说这个工具非常强大。如果说评测机是狂轰滥炸的飞弹,那么junit就是一把可以精确打击的匕首,也许你可以侥幸逃过狂轰滥炸,但是你绝对逃不过那精确一击。

OO第三单元总结——JML

一般junit测试所用样例都是自己精心构造的数据。随着代码不断完善进行补充。最方便的一点是:在每次版本更新后,都可以用junit一键回归测试,看是否改错了某些地方,可以说是非常强大的工具。

OO第三单元总结——JML

此外,junit还可以在运行的时候检测代码覆盖率,我们可以看到哪些地方被测试过,哪些地方还没有做测试,方便之后针对那些没有被覆盖的地方,继续补充测试样例。

openjml的使用

使用openjml工具可以对代码进行静态检查,有时候可以发现一些非逻辑错误导致的问题。比如我在第九次作业中出现的减法溢出的问题,其实是可以用openjml发现的,但当时对这种工具的使用还不是很了解,所以导致出现了bug。这也更加证明了在一个工程中,做好充分测试的必要性,不要让一个庞大的工程因为一个细小的错误而全盘崩塌。