oo第三单元总结
作者：互联网
oo第三单元总结
一. 梳理JML语言的理论基础、应用工具链情况
(1) JML理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言，基于Larch方法构建。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规 格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
· JML常用方法规格
（1）requires子句定义该方法的前置条件(precondition)
（2）assignable列出这个方法能够修改的类成员属性，用于副作用范围限定。\nothing是个关键词，如果用\nothing表示这个方法不对任何成员属性进行修改，是一个pure方法。
（3）ensures子句定义了后置条件。
（4）signals子句，signals子句的结构为 signals (***Exception e) b_expr ，意思是当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e。还有一个简化的signals子句，即signals_only子句，后面跟着一个异常类型。signals子句强调在对象状态满足某个条件时会抛出符合相应类型的异常；而signals_only则不强调对象状态条件，强调满足前置条件时抛出相应的异常。
· JML常用类型规格
不变式invariant
状态变化约束constraint
· JML常用表达式
\result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
(2）应用工具链情况
OpenJML：使用SMT Solver来对检查程序实现是否满足所设计的规格。
IDEA静态检查插件官网链接：https://plugins.jetbrains.com/plugin/11072-openjml-esc
OpenJML静态检查网页：https://www.rise4fun.com/OpenJMLESC/MaybeAdd
Eclipse安装OpenJML一个Location网址：http://jmlspecs.sourceforge.net/openjml-updatesite/
JMLUuitNG：可根据规格自动化生成测试样例，进行单元测试。
官网链接：http://insttech.secretninjaformalmethods.org/software/jmlunitng/
二. 部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果
OpenJML使用SMT Solver来对检查程序实现是否满足所设计的规格。
对JML的检查，可以分为语法检查，静态检查和动态检查。
openjml -check <source files>
openjml -esc <source files>
openjml -rac <source files>
为解决因找不到其他类而产生的很多不应出现的报错，使用IDEA将工程打包为jar包，使用openjml -cp 的方式执行语法检查。比如：
openjml -esc -cp oohomework10.jar src/com/oocourse/specs2/MyGraph.java
但这样仍会造成一些报错，比如：java.io.IOException: Stream closed
· 部署SMT Solver
ubuntu安装OpenJML后即可使用。
IDEA 官网下载OpenJML插件安装重启IDEA，配置在File -> Settings -> Other Settings -> JML Checker，我的配置大致如下：
Eclipse安装在Help -> Install New Software，Location可参考http://jmlspecs.sourceforge.net/openjml-updatesite/。配置在Window ->Perferences -> OpenJML -> OpenJML Solvers，我的配置大致如下：
· 对三个方法尝试验证
对第十次作业的MyGraph类进行验证：
Could not find model field theObject：找不到模型字段。可能是Openjml不支持这种类型转换。
对第十次作业的MyMap类进行验证（IDEA Check ESC)：
仍是找不到模型字段的错误，但警告很多，只要涉及到我定义的变量都会有警告。比如：
也有如下前置条件为假的警告，我不太清楚是因为什么：
对第十一次作业MyMap类进行验证：
证明者不能建立断言，可能存在溢出等问题。
三. 部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析
在应用JMLUnitNG的过程中，我一直不能在Windows系统上装上openjml和jmlunitng，最后我装了ubuntu。
以下是几篇有关安装ubuntu和在ubuntu上运行jmlunitng的参考资料：
WSL(Windows Subsystem for Linux)的安装与使用
apt - Trying To Install Java 8.. Unable to locate package openjdk-8-jre - Ask Ubuntu
安装完成后，可使用IDEA将工程打包为jar包，可参考：
打包完成后可执行（我这里的oohomework10.jar是打包后的jar包）:
jmlunitng -cp oohomework10.jar src/com/oocourse/specs2/MyGraph.java
生成文件大致如下：
运行MyGraph_JML_Test.java，可得到运行结果：
测试用例大部分采用边界数据，可以较为全面地测试代码的覆盖度。
观察Failed的测试用例，将其在IDEA中测试，得到Failed, invalid path.可能是程序对于一些数量有限制，也可能我的代码中还存在什么问题。
四. 按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
第九次作业：
第九次作业逻辑较为简单，注意将DISTINCT_NODE_COUNT的计算放在指令条数较少的PATH_ADD和PATH_REMOVE等指令执行的函数中，避免CPUTIME超时。
第十次作业：
第十次作业在第九次作业的基础上加入图的概念，我采用的是Floyd算法，用静态二维数组存储图。
第十一次作业：
第十一次作业在上一次作业的基础上添加几个功能，我采用的是不拆点的方法，最短路径用Dijistra算法计算，图仍使用静态数组存储。
在这三次作业中，基本每一次只是在上一次的代码中添加代码，以实现新的功能，最大的变化是第十次作业到第十一次作业最短路径算法由Floyd换成Dijistra。
五. 按照作业分析代码实现的bug和修复情况
第九次作业：
强测测试点出现CPU_TIME_LIMIT_EXCEED，是因为用arraylist插入删除时间复杂度过高，以及在getDistinctNodeCount()函数中统计数量，每次调用都重新统计，用时过多。
bug修复中将arraylist改为hashmap，getDistinctNodeCount()函数中统计数量操作放到add和remove函数中了。
第十次作业：
用Flody算法时循环次数过少，错误代码是图中有几个点就循环几次，但在操作中会出现节点最大序号与节点数不同的情况，导致有的点没有被算进图中。
第十一次作业：
我修改前的代码对于一条路径中的环路，采用加入新边的方法，但是对于加入的新路径中仍有环路的情况无法处理。
比如：
PATH_ADD 6 4 11 1 4 1 8 14 6 2
LEAST_UNPLEASANT_VALUE 1 2
正确答案是528，走1，4，6，2
我会输出532，走1，11，4，6，2
修改后采用每条路径建一个小图，先计算小图内部的最短路径，然后加入大图。
对于强测中的CPU_TIME_LIMIT_EXCEED，是因为我加入路径时，如果一条路径中环路很多，会消耗很长时间。
六. 阐述对规格撰写和理解上的心得体会
对于规格的撰写，我认为规格的确能使我更加清晰地理解方法的作用，也便于发现代码中的错误。但实际在应用中，我应用Junit设计的测试样例很局限，用OpenJML会报很多我也不是很明白的错误，比如找不到符号，可能和真正的错误混杂在一起，让我很难分辨。
这三次作业单凭我手动找bug，真的很难找到全部的bug，还是应该多理解规格的用途和多测试。
标签：oo,总结,OpenJML,作业,IDEA,规格,JML,openjml,单元 来源： https://www.cnblogs.com/xpppx/p/10907755.html