OO之旅——JML篇
目录
- OO第三单元总结
- 1. JML语言理论基础以及应用工具链情况梳理
- 2. OpenJML的简单使用:部署、验证及结果分析
- 3. JMLUnit的使用:部署、验证及结果分析
- 4. 作业架构设计梳理
- 5. bug分析及修复情况
- 6. 心得体会
OO第三单元总结
1. JML语言理论基础以及应用工具链情况梳理
1.1 JML语言理论基础
JML(Java Modeling Language)是一种用于规范Java程序行为的行为接口规范语言。JML为方法和类型的规格进行定义,为程序的形式化验证提供了基础,通过工具链可以实现静态检查和自动测试数据生成。
注释结构
- 行注释:
// @ annotation
- 块注释:
/* @ annotation @*/
JML表达式
- 原子表达式
- \result,\old( expr )
- 量化表达式
- \forall表达式:全称量词修饰的表达式
- \exists表达式:存在量词修饰的表达式
- \sum表达式:返回给定范围内的表达式的和
- \max表达式:返回给定范围内的表达式的最大值
- \min表达式:返回给定范围内的表达式的最小值
- 集合表达式
- 可以在JML规格中构造一个局部的集合(容器),明确集合中可以包含的元素。
- 操作符
- 子类型关系操作符: E1<:E2 ,
- 等价关系操作符: b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2
- 推理操作符: b_expr1== >b_expr2 或者 b_expr2< ==b_expr1
- 变量引用操作符:\nothing指示一个空集;\everything指示一个全集
方法规格
- 前置条件(pre-condition)
- 通过requires子句来表示: requires P;
- 后置条件(post-condition)
- 通过ensures子句来表示: ensures P;
- 副作用范围限定(side-effects)
- 使用关键词 assignable 或者 modifiable
类型规格
- 不变式invariant
- 状态变化约束constraint
1.2 工具链简介
与规格化设计相关的工具主要有:OpenJML, JMLUnit, TestNG等等。
- OpenJML
对Java 编译器将带有 JML 规范注释的 Java 程序编译成 Java 字节码。 编译的字节码包括检查的运行时断言检查指令。
- JMLUnit与TestNG
JMLUnit 与 TestNG主要是基于JML规格生成样例并自动化进行单元测试
2. OpenJML的简单使用:部署、验证及结果分析
参考伦佬的贴子。
2.1 JML规格语法check
源码
public class Demo {/*@@ public normal_behaviour@ requires lhs<0 &&*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(114514, 1919810);}
}
结果分析
$ ./openjml -check Demo.java
Demo.java:5: 错误: The type or expression near here is invalid (or not implemented): ( token <JMLEND> in JmlParser.term3())*/^
1 个错误
检测出JML表达式无效。
2.2 基于OpenJML的静态bug检测
源码
public class Demo {/*@@ public normal_behaviour@ requires lhs > rhs;@ ensures \result > 0;@ also@ requires lhs < rhs;@ ensures \result < 0;@ also@ requires lhs == rhs;@ ensures \result == 0;@*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(114514, 1919810);}
}
结果分析
$ ./openjml -check Demo.java
$ ./openjml -esc Demo.java
Demo.java:14: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compare: underflow in int differencereturn lhs - rhs;^
demo/Demo.java:14: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compare: overflow in int differencereturn lhs - rhs;^
2 warnings
检测结果显示JML表达式合法,但存在减法溢出的漏洞。
2.3 运行时检查
源码
public class Demo {/*@@ public normal_behaviour@ requires lhs > rhs;@ ensures \result > 0;@ also@ requires lhs < rhs;@ ensures \result < 0;@ also@ requires lhs == rhs;@ ensures \result == 0;@*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(2147483647, -2147483647);}
}
结果分析
94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ ./openjml -rac Demo.java94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ java -Djava.ext.dirs=lib Demo
Demo.java:14: 警告: JML result of numeric operation is out of range of the target typereturn lhs - rhs;^
Demo.java:13: 警告: JML postcondition is falsepublic static int compare(int lhs, int rhs) {^
Demo.java:5: 警告: Associated declaration: Demo.java:13: 注:@ ensures \result > 0;^
openjml 的使用和 javac 大致相同,先编译后运行即可。结果显示出现了减法溢出的情况。
3. JMLUnit的使用:部署、验证及结果分析
参考伦佬的贴子——第二篇。
以下是针对MyPath中的部分方法进行测试
3.1 生成测试文件
3.2 编译
编译部分共分为两步:
- 用 javac 编译 JMLUnitNG 的生成文件
- 用 jmlc 编译自己的文件,生成带有运行时检查的 class 文件
94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ javac -cp jmlunitng.jar src/*.java94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ ./openjml -rac src/MyPath.java
3.3 测试及结果分析
94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml/src
$ java -Djava.ext.dirs=../lib MyPath_JML_Test
[TestNG] Running:Command line suitePassed: racEnabled()
Failed: constructor MyPath(null)
Skipped: <<null>>.containsNode(-2147483648)
Skipped: <<null>>.containsNode(0)
Skipped: <<null>>.containsNode(2147483647)
Skipped: <<null>>.getDistinctNodeCount()
Skipped: <<null>>.getNode(-2147483648)
Skipped: <<null>>.getNode(0)
Skipped: <<null>>.getNode(2147483647)
Skipped: <<null>>.isValid()
Skipped: <<null>>.size()===============================================
Command line suite
Total tests run: 11, Failures: 1, Skips: 9
===============================================
由结果可知,MyPath的构造未通过测试,经查,发现,当传进来的nodeList为空时,在 nodeList.length
时可能会发生访问空指针的错误。
public MyPath(int... nodeList) {for (int i = 0; i < nodeList.length; i++) {myNodes[i] = nodeList[i];}}
4. 作业架构设计梳理
4.1 第一次作业
分析
第一次作业较为简单,利用好HashMap实现 O(1) 的查询即可。
类图如下:
- MyPath
- 使用
ArrayList<Integer> nodes
结构保存节点序列 - 使用
HashMap<Integer, Integer> nodesMap
来保存结点及结点在path中的出现次数,以便由nodesMap.size()
直接getDistinctNodeCount()
- 使用
- MyPathContainer
- 使用
HashMap<Integer, MyPath> id2Path
和HashMap<MyPath, Integer> path2Id
两个HashMap来实现Path
与PathId
的双向映射,从而快速索引。
- 使用
4.2 第二次作业
分析
- 第二次作业在
PathContainer
的基础上新增了Graph
接口,MyPathContainer
无需重构,直接继承即可。 - 需要注意的是由于增删指令不超过80条,查询指令将接近7000条,而评测又严格限制CPU时间,因此最短路的计算就需要一定的策略了。考虑到查询指令数,如果采用Floyd每次都把所有结点的最短路算出来,将会产生大量的性能浪费,同时由于其O(n^3)的复杂度,因而弃用。
- 考虑到第二次作业为无边无权图,本人采用 BFS + Lazy Search 算法。即类似缓存机制,将答案存储在“TLB”中,每次进行增删操作时由于图结构改变,需要清空TLB。每次查询先查TLB,若命中,直接返回;若MISS,就BFS一下同时更新TLB。
类图如下:
- Edge
- 抽象出来的无向边,存储两个结点以及边权(本次作业恒为1)
- 重写equals及hashcode方法
- MyGraph
- 使用
HashMap<Integer, Integer> nodeMap
和HashMap<Edge, Integer> edgeMap
来存储结点和边及其度数 HashMap<Edge, Integer> weight
和HashMap<Edge, Integer> shortestDist
分别存储权重即相应的最短路
- 使用
4.3 第三次作业
本次作业难度有了较大的提升,且由于当周冯如杯答辩等原因导致时间紧迫,加上周一晚上盲从讨论区大佬的观点。在没有完全参悟拆点法的情况下,临时更换策略极限重构,结果在建图时遇到了很大的困难,最后因为时间关系草草完成了图的构建,由于结构混乱,且复杂度较高,导致强测大半CTLE。真应了助教那句:
“重构一时爽,一次重构火葬场”
由于没有将图结构的存储与答案的存储分离开,导致二者的耦合度较高,维护成本非常大;
因而在认真研究了标程的架构设计后,重构了图的存储逻辑,借鉴了标程的工厂模式,如下。
分析
- 本次作业采用了 拆点 + Dijkstra + Lazy Search,大体思路同上次作业,拆点遵从zyy大佬的
2+x
模式,具体见这里。 - 难点之一在于四个最短问题的求解,而它们的主要区别在于邻接边与换乘边的权值不同,设邻接边权为x,换乘边权为y,则有:
- 最短路径:x = 1, y = 0 // 实际上,最短路径的求解我仍然放在了 MyGraph 中
- 最少换乘:x = 0, y = 1
- 最低票价:x = 1, y = 2
- 最小不满意度:x =
MAX( F(fromNode), F(toNode) )
, y = 32;
- 难点之二则在于图的存储,本人采用了嵌套HashMap以邻接表的形式来存储。设计模式上,重构版采用了工厂模式,将三种最短问题抽象为同一种产品,不同的仅仅是
stepWeight
与switchWeight
,同时由于最少不满意度的邻接边权非固定值,需要单独对其进行拓展,处理stepWeight
的求解。这里仅仅需要继承RailwayGraphFactory
即可,这样在MyRailwaySystem
中只需要维护好这三个产品即可。 - 跨越上面两座大山后,问题基本就已经解决了,唯一仍需注意的是Dijkstra的写法,本人原始写法在更新dist[]时是无脑遍历所有结点,而拆点法会导致节点数最大会达到4000+,因而时间巨慢。实际上,每次遍历只需要遍历离源点st最近结点vertex的可达集即可大大降低时间复杂度。
类图如下:
- RailwayGraphFactory
public static final int INFINITY = 0x3fffffff;private final int stepWeight; // 邻接边权private final int switchWeight; // 换乘边权// <stNode, edNode> -> edgeWeightprivate HashMap<Node, HashMap<Node, Integer>> adjList = new HashMap<>();// <fromNode, toNode> -> shortest distanceprivate HashMap<Node, HashMap<Node, Integer>> ansMap = new HashMap<>();
- MyRailwaySystem
/* Abstract Graph */
// <NodeId, stNode> : pathId = 0
private HashMap<Integer, Node> stMap = new HashMap<>(); // 抽象起点
// <NodeId, edNode> : pathId = -1
private HashMap<Integer, Node> edMap = new HashMap<>(); // 抽象终点/* weight matrix */
private RailwayGraphFactory transferMatrix; // 最少换乘
private RailwayGraphFactory priceMatrix; // 最低票价
private UnpleasantGraphFactory unpleasantMatrix;// 最小不满意度
5. bug分析及修复情况
- 第一次作业中的compareTo出现了减法溢出错误。原因是采用了一种比较“取巧”的做法
return a-b;
,由于第一次作业比较掉以轻心,没有进行有效的测试,导致强测WA了快一半点。修复时只需改用if-else
即可。 - 第二次作业在强测与互测中均未被发现bug。
- 第三次作业即在3.3陈述的CTLE错误,莫得办法,只能重构
(捂脸),但在重构的过程中也确实有所收获。
6. 心得体会
三周的JML之旅已然结束,这期间当然又踩了很多坑,也吃了不少经验教训。
首先,给我留下印象最深刻的还是那句话,“重构一时爽,但也可能一次重构火葬场”。不过虽然如此,在重构的过程中也有了很多新的感悟与体会,一个优美的架构好处不仅仅在于其可扩展性,由于模块与模块之间耦合度低,逻辑重合度低,其bug调试及定位难度也大幅降低,同时也能更好的借助JUnit进行覆盖性测试。
下面再来谈一谈对JML规格撰写的体会。
通过查阅JML手册以及参考已有规格,为一个方法写一份简单的规格描述难度并不大,在几次上机中也并没有太大的问题,而想要针对某个特定项目写一份完整、严谨的规格却是十分困难的。但 JML 的好处在于,测试人员能够从设计层面直接判断方法的正确性,而不用花费大量时间阅读代码。同时由于其语法的严谨性、规范性,给开发人员也带来极大地便利,不需要再去啃模棱两可的指导书中的需求,专注于代码的编写,正如指导书所言,”只要你确保满足了JML的需求,那么你的程序一定是正确的“。
此外,通过对 JML 规格的阅读与撰写,我对每个方法的 Pre-Condition, Post-Condition, Side-Effect
有了更加深刻的理解,这是一个方法,或是一段程序正确性的根本保证,能更好地帮助我们判断一个架构设计的正确性与合理性。
最后再谈一谈Openjml。本单元一开始对基于JML规格的形式化验证与自动化测试是充满期待的,但不得不说,JML的工具链使用体验极差,对语法的要求过于苛刻,导致写一份能够完美通过编译的JML规格的难度要远远大于完成程序本身,似乎有些本末倒置?但 JML 教给我们规格设计的思想以及这种规范编程的思维方式,对我们的程序员进化之路是大有裨益的。
国际惯例,祝OO课程越来越好!
转载于:https://www.cnblogs.com/puzzledAtticus/p/10908088.html
OO之旅——JML篇相关推荐
- React Native填坑之旅--动画篇
React Native填坑之旅--Button篇 React Native填坑之旅--动画 React Native填坑之旅--HTTP请求篇 动画是提高用户体验不可缺少的一个元素.恰如其分的动画可 ...
- 第一学期ACM之旅总结篇
是我大一第一学期ACM之旅总结篇鸭,纪念逝去的青春: 自加入ACM集训队以来已有三个月之久,虽然一开始什么都不懂,但对ACM充满期待与向往.入队以后,通过和队员们一起学习以及各个学长的指导下,我慢慢地 ...
- Linux之旅----硬件篇
linux之旅----硬件篇(DIY) 记得第一次接触电脑应该是小学三年级,那时候的它对我来说只是一个游戏机的概念:极品飞车.红色警戒.CS.热血传奇.......陪我度过了小学懵懂的时光:泡泡堂.梦 ...
- CTF之旅WEB篇(3)--ezunser PHP反序列化
一.审题 对方朝你扔过来一串代码(当然这次又是蹭的题只说过程和思路): <?php highlight_file(__FILE__); class A{public $name;public $ ...
- ABAP项目砖家之旅-基础篇
ABAP项目砖家之旅-基础篇 前言 一.ABAP简介 二.ABAP开发工具 1.SAPgui 2.eclipse和HANA studio 三.相关搬砖经验 1.必须还是熟悉语法 2.复制粘贴写注释 3 ...
- ESP8266开发之旅 网络篇⑭ web配网
文章目录 1. 前言 2. Web配网(AP配网) 2.1 自定义AP配网 2.2 WiFiManager 3. 总结 授人以鱼不如授人以渔,目的不是为了教会你具体项目开发,而是学会学习的能力.希望大 ...
- [OO] Unit3 Summary JML系列
文章目录 [OO] Unit3 Summary JML系列 JML理论基础 优点 语法基础 常用表达式 方法规格 类型规格 JML工具链 测试工具使用报告 SMT Solver EvoSuite JM ...
- ESP8266开发之旅 应用篇⑭ 局域网应用 ——炫酷RGB彩灯(WebSocket实现)
文章目录 1.前言 2.技术原理 3.ESP8266 源码 4. APP 授人以鱼不如授人以渔,目的不是为了教会你具体项目开发,而是学会学习的能力.希望大家分享给你周边需要的朋友或者同学,说不定大神成 ...
- ESP8266开发之旅 应用篇⑧Arduino版本 WiFi杀手
文章目录 1. 前言 授人以鱼不如授人以渔,目的不是为了教会你具体项目开发,而是学会学习的能力.希望大家分享给你周边需要的朋友或者同学,说不定大神成长之路有博哥的奠基石... 共同学习成长QQ群 62 ...
最新文章
- Python基本语法_变量作用域LEGB
- 数据库及中间件术语解释
- 一个前端博客(9)——浏览器检测和加载
- 12月第2周业务风控关注 | 公安部:严打自媒体“网络水军”违法犯罪,关闭大V账号1100余个...
- Python 编写规范
- 科学道德与学风-2021雨课堂答案-第1章
- 图灵好书推荐——数学+物理+宇宙
- 浏览器 pad android,360安全浏览器平板电脑Pad专用版-360安全浏览器HD 安卓版v1.1.0-PC6安卓网...
- 解决拯救者Y7000打游戏,看视频没有声音的问题
- 重要文件即时搞定,不用插电就能打印,汉印MT800移动便携打印机上手
- 【用EXCEL编写俄罗斯方块小游戏(基于VBA)】
- 关于日记账导入-外币
- ios上传ipa:Xcode导入ipa上传至App Store
- [USACO 2010 Feb S]Chocolate Eating
- 美国签证(B1)经验总结
- JQuery 模糊匹配(JQuery 选择器模糊匹配、选择指定属性是以给定字符串开始的元素 )
- Cruzer Profile 原理分析
- Python对3D STEP/STP 文件解析
- linux运维工程师视频教程一(下)-张彬-专题视频课程
- html表白页面抖音,抖音表白代码
热门文章
- 竞拍商城APP开发有什么功能
- vc++ 2010错误 IntelliSense: 无法打开 源 文件 stdafx.h
- Oracle数据库将时间戳转换成年月日时分秒格式
- android 多套布局适配,Android屏幕适配 重点盘点
- 一天一点raknet_Editing 教程/WebSocket
- 数据库里怎么修改服务器爆率,关于数据库点窜爆率及点窜和增加掉落的教程(纯小白版)...
- kies air java 证书_Java ToStringBuilder類代碼示例
- c语言银行卡管理系统实验报告,C++编写的简单银行卡管理系统
- ffmpeg之demux 解复用
- 3a2b递归排列java,高考数学解题技巧-递推数列通项公式的十种策略例析