OO第三单元 JML规格 单元回顾
写在前面
这一单元的作业看似难度比前两单元下降很多,但一不小心就会出各种问题...第二次作业留下了惨痛的教训。
一. JML语言的理论基础、应用工具链
理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言(Behavior Interface Specification Language,BISL),基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工作,并融入了Betrand Meyer, John Guttag等人关于Design by Contract的研究成果。近年来,JML持续受到关注,为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具,不仅可以基于规格自动构造测试用例,并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。
原子表达式
\result : 非void型方法执行结果。
\old(expr) : 表示表达式expr在相应方法执行前的取值。该表达式涉及到评估 expr 中的对象是否发生变化,但是针对一个对象引用而言,只能判断引用本身是否发生变化,而不能判断引用所指向的对象实体内容是否发生变化。
\not_assigned(x,y,…) : 用来表示括号中的变量是否在方法执行过程中被赋值。该表达式主要用于后置条件的约束表示上(限制一个方法的实现不能对列表中的变量进行赋值)。
\not_modifed(x,y,…) : 表达式限制括号中的变量在方法执行期间的取值未发生变化。
\nonnullelements(container) : 表示 container 对象中存储的对象不会有 null。
\type(type) : 返回类型type对应的类型(Class)。e.g. type( boolean )为Boolean.TYPE
\typeof(expr) : 该表达式返回expr对应的准确类型。e.g. \typeof( false )
量化表达式
\forall : 全称量词修饰的表达式,表示对于给定范围内的元素,每个元素都满足相应的约束。
\exists : 存在量词修饰的表达式。
\sum : 返回给定范围内的表达式的和。
\product : 返回给定范围内的表达式的连乘结果。
\max : 返回给定范围内的表达式的最大值。
\min : 返回给定范围内的表达式的最小值。
\num_of : 返回指定变量中满足相应条件的取值个数。
操作符
分为子类型关系操作符、等价关系操作符、推理操作符、变量引用操作符
方法规格
方法规格的核心内容包括三个方面:前置条件、后置条件和副作用约定。
前置条件 : 对方法输入参数的限制,不满足则不能保证正确性。
后置条件 : 对方法执行结果的限制,执行后如果满足则执行正确。
副作用约定 : 指方法在执行过程中对输入对象或 this 对象进行了修改(对其成员变量进行了赋值,或者调用其修改方法)。
方法在执行过程中会修改对象的属性数据或者类的静态成员数据,从而给后续方法的执行带来影响。从方法规格的角度,必须要明确给出副作用范围。、
注1:不允许在副作用约束子句中指定规格声明的变量数据。
注2:private量通常调用者不可见。可以用/*@ spec_public @*/注释一个类的私有成员变量,表示在规格中可以直接使用,从而调用者可见。
具体JML学习博客如下:
应用工具链:
OpenJML: OpenJML
Junit4: 在 IDEA 中 使用 JUnit4
JMLUnitNG: JMLUnitNG Release History
二. 部署JMLUnitNG
首先感谢大佬的博客https://www.cnblogs.com/pekopekopeko/p/12920417.html, 以及几位不愿意透露姓名的大佬的指点。在部署JMLUnitNG时遇到了很多自己无法解决网络上又搜不到的问题。运行得到的结果如下,由于该类和方法较为简单,故可能实际效果和自己编造或随机生成差不多,但如果在大规模的代码中,JMLUnitNG应该会有更广泛的应用。可以看到,JMLUnitNG会对很多边界情况,以及null值进行测试,效果很好。
[TestNG] Running: Command line suite Failed: racEnabled() Passed: constructor MyGroup(0) Passed: constructor MyGroup(-2147483648) Passed: constructor MyGroup(2147483647) Failed: <<MyGroup@3f0861b4>>.addPerson(null) Failed: <<MyGroup@40ea37bc>>.addPerson(null) Failed: <<MyGroup@ce6451f3>>.addPerson(null) Passed: <<MyGroup@6dce12b0>>.addPerson(java.lang.Object@a741e380) Passed: <<MyGroup@352ef8b1>>.addPerson(java.lang.Object@413695ef) Passed: <<MyGroup@94e06b7c>>.addPerson(java.lang.Object@3c2a79bf) Passed: <<MyGroup@9d62ce71>>.getId() Passed: <<MyGroup@5ec703d1>>.getId() Passed: <<MyGroup@039cd84b>>.getId() Passed: <<MyGroup@31cb5780>>.equals(null) Passed: <<MyGroup@97c5d04b>>.equals(null) Passed: <<MyGroup@5a14c09>>.equals(null) Passed: <<MyGroup@0c148239>>.equals(java.lang.Object@1ef9670c) Passed: <<MyGroup@058329f6>>.equals(java.lang.Object@5ab86c79) Passed: <<MyGroup@60215eee>>.equals(java.lang.Object@8c2b740e) Passed: <<MyGroup@4b508297>>.getRelationSum() Passed: <<MyGroup@1c2c22f3>>.getRelationSum() Passed: <<MyGroup@5c68e983>>.getRelationSum() Passed: <<MyGroup@d4a16cb0>>.getValueSum() Passed: <<MyGroup@ae2c9538>>.getValueSum() Passed: <<MyGroup@d204ae3f>>.getValueSum() Passed: <<MyGroup@1abf43c2>>.getAgeMean() Passed: <<MyGroup@8510ba23>>.getAgeMean() Passed: <<MyGroup@957ec4f0>>.getAgeMean() Passed: <<MyGroup@1906ab8d>>.getAgeVar() Passed: <<MyGroup@2e168542>>.getAgeVar() Passed: <<MyGroup@1a8572d0>>.getAgeVar() Passed: <<MyGroup@0d8f342c>>.getConflictSum() Passed: <<MyGroup@2cfdb15a>>.getConflictSum() Passed: <<MyGroup@9ebdc26f>>.getConflictSum() =============================================== Command line suite Total tests run: 34, Failures: 4, Skips: 0 ===============================================
三. 梳理自己的架构设计
第九次作业
UML图
代码行数
第九次作业较为简单,MyGroup中采用一个Arraylist保存people(为第十次的bug埋下伏笔),MyPeople分别采用一个HashMap保存acquantance和value。其余部分都是直接翻译JML。
其中,复杂度比较高的方法为iscircle。采用循环实现的广度优先搜索实现该方法。
第十次作业
UML图
代码行数
第十次作业将各类arraylist改为HashSet,同时本着“以空间换时间”的原则,MyNetwork里建立一个HashSet来保存People,同时建立了一个HashMap来保存id和people的映射信息,便于访问和查询。
同时第十次作业中复杂度比较高的方法为iscircle,由于有时间要求,故改进了第九次的bfs。同时对于Group里的各种方法,采用缓存机制,设立relationSum,valueSum,ageSum,conflictSum属性来缓存信息,addtogroup时更新上述信息。当add relation时,如果id1和id2在相同的group里,则更新这些group里的缓存信息,相应方法时直接返回值即可。同时由于add relation会经常用到,为了快速查询id1和id2是否在相同的group里,在MyPeople类里设立HashSet<Integer> groupId属性来保存当前people加入的group,查询id1和id2是否在相同的group里时,直接调用retainAll方法,来提高效率。
第十一次作业
UML图
代码行数
第十一次作业沿用了第十次作业的架构,MyGroup类里delperson时更新相应缓存信息,MyNetwork里建立money属性来实现新增的与money有关的两个方法。
为了出现了QueryBlockSum方法,采用并查集实现,并将iscircle方法也改为并查集。新建blocksum属性来缓存信息,add person是blocksum++,add relation时,如果id1和id2的根不相同,则blocksum--。
对于qmp方法,则采用优先队列优化的dijkstra算法实现,新建一个类来保存<Id , value>的映射信息(即保存对应边及其权值),并重写equals、hashcode、compareTo方法。
对于qsl方法,本菜鸡没理解tarjan算法de不出bug,于是只能使用暴力枚举来删节点。首先通过dfs找到一条路径,将该路径上的节点依次删除。若出现不连通,则证明不双连通。同时优化dfs方法,在退出某一节点时,不取消标记该节点,从而提高dfs的性能。
四. bug修复情况
第九次作业、第十一次作业强测互测均未出现bug。
第十次作业,由于在Network类里保存people时用了arraylist方法导致了很多点超时,换成hashmap以后即修复bug。
三次作业均采用python随机生成数据来hack,hack到的bug大都因为超时导致。
在完成第十一次作业时,qsl里的dfs方法的效率一直很低。200个people,200条relation时就要运行很久,800个人people,800条relation时几乎不能出结果。最后发现问题全在dfs,当数据一大时dfs的复杂度会指数上升。原因在于我在dfs里设立一个visited变量保存当前遍历的节点,dfs开始时将当前节点add入visited,dfs结束回溯时将该节点remove出visited,之后发现无须移除。因为回溯已经代表当前节点和目标节点不连通,那意味着当前节点已经无须再访问,无论从哪个节点到达该节点都不可能到达目标,所以只要在dfs开始时将当前节点add入visited,dfs结束时准备回溯时无须移除,效率则能大幅提高。
五.心得体会
在本次作业中,体会到了JML规格对于大规模开发的好处,但并未感受到junit、JMLunitNG对于自动测试的好处。或许是因为我们本单元作业代码量不大、内容简单、情况少,写junit的效率反而没有随机生成自动数据对拍来得快和直接。但如果代码量一大,想必junit的优势就能体现出来。
第十次作业的强测让我的心态一度崩溃,各种优化结果还是被一个隐藏的二重循环害惨。第十一次次作业对算法要求很高,数据结构时没有亲自写过的堆优化dijkstra、并查集,在第十一次作业里都实现了,也对java语言的各种内置容器有了更加深入的了解,对图论算法也更加熟悉。虽然对第十次作业的成绩并不满意,但也吸取了教训。不管怎么说,总算挺到了最后一单元,加油加油~
原文地址:https://www.cnblogs.com/wtrwtr/p/12931690.html
- JavaScript 教程
- JavaScript 编辑工具
- JavaScript 与HTML
- JavaScript 与Java
- JavaScript 数据结构
- JavaScript 基本数据类型
- JavaScript 特殊数据类型
- JavaScript 运算符
- JavaScript typeof 运算符
- JavaScript 表达式
- JavaScript 类型转换
- JavaScript 基本语法
- JavaScript 注释
- Javascript 基本处理流程
- Javascript 选择结构
- Javascript if 语句
- Javascript if 语句的嵌套
- Javascript switch 语句
- Javascript 循环结构
- Javascript 循环结构实例
- Javascript 跳转语句
- Javascript 控制语句总结
- Javascript 函数介绍
- Javascript 函数的定义
- Javascript 函数调用
- Javascript 几种特殊的函数
- JavaScript 内置函数简介
- Javascript eval() 函数
- Javascript isFinite() 函数
- Javascript isNaN() 函数
- parseInt() 与 parseFloat()
- escape() 与 unescape()
- Javascript 字符串介绍
- Javascript length属性
- javascript 字符串函数
- Javascript 日期对象简介
- Javascript 日期对象用途
- Date 对象属性和方法
- Javascript 数组是什么
- Javascript 创建数组
- Javascript 数组赋值与取值
- Javascript 数组属性和方法
- PHP getID3类的使用方法学习笔记【附getID3源码下载】
- PHP读取Excel内的图片(phpspreadsheet和PHPExcel扩展库)
- 浅谈laravel 5.6 安装 windows上使用composer的安装过程
- PhpStorm 如何优雅的调试Hyperf的方法步骤
- 在TP5数据库中四个字段实现无限分类的示例
- 详解Laravel设置多态关系模型别名的方式
- tp5修改(实现即点即改)
- 自定义Laravel (monolog)日志位置,并增加请求ID的实现
- PHP的Trait机制原理与用法分析
- 如何在centos8自定义目录安装php7.3
- 基于laravel belongsTo使用详解
- laravel model模型定义实现开启自动管理时间created_at,updated_at
- laravel ORM关联关系中的 with和whereHas用法
- thinkPHP事务操作简单案例分析
- php 多个变量指向同一个引用($b = &$a)用法分析