OO第三次作业总结

梳理JML语言的理论基础、应用工具链情况

JML语言有点类似于离散数学，用规范化的方式去描述类的属性以及方法。
存在形式
一般都是以

//@ -----
/*@ ----- @*/

这两种形式存在
方法规格
方法规格是描述一个方法的，主要可以分为requires,assignable, ensures三个部分。
requires是保证方法的前置条件，也就是调用者需要保证的参数
assignable是副作用，即什么变量可能会被改变。如果没有改变可以不写
ensures是说明方法后满足的要求以及返回值所满足的条件。通常来讲是唯一存在的。
对于会抛出异常的方法，还会有normal_behavior以及exception_behavior，如果一个方法不存在requires和assignable，也可以用pure进行修饰
数据规格
数据规格分为invariant和constraint。前者是时时刻刻数据都要保持的条件；后者是状态修改前后（方法运行前后）的状态的变化的约束。
表达式
JML常用的表达式

名称	作用
esult	代表方法的返回值
old	方法操作前这个变量的值
forall	(forall a;b;c) 对所有的a，在b的条件下，都有c == true
exists	(exists a;b;c) 存在a，在b的条件下，都有c == true
sum	(sum a;b) 对所有满足a条件的情况，对b进行求和

JML工具链

SML solver：代码检查等价性（一直在进行报错）
JMLUnitNG：代码的（不是很好用的）自动化检查
JMLUnit：代码的手动写测试样例的检查

OPENJml SMT solver的尝试

通过焦佬的博客 https://www.cnblogs.com/pekopekopeko/p/12920417.html 完成了一次不知道有没有成功的尝试。
第一次尝试没有进行更改，应该是没有识别出HashMap，出现了报错。（不清楚其他地方检查的怎么样）

第二次对所有的容器进行了更改，它的报错变得更加的奇怪。

JMLUnitNG

根据上述博客进行修改我碰到的问题有：不识别package 不识别三目运算符和一些不识别小于等于号的问题。。
进行了删除之后再进行测试结果如下

框架梳理

以第三次作业为例，UML如图

可能还是没有办法跳出对着JML规范写程序的感觉，除非特别困难的函数可能会用新建类和用几个方法共同实现。

bug

第一次作业还好
第二次作业没有仔细查看所有JML，三目运算符有遗漏导致没有进强测
因为是自己随机构造代码，所以会有很多ap和ag在最前面，就略过这几个三目运算符了。
第三次作业主要是没有平衡好算法的时间，计算错了一个方法的时间效率，导致大面积CTLE，同时重新书写了一些方法导致思考不全面，而且随机构造代码只考虑了ap和ag，没有考虑ar需要一定的数量所以随机代码参考价值不大。

心得体会

JML感觉还是只停留在概念，没有办法跳脱出JML外去思考这些问题。一个是担心漏掉条件，其次还是没有将JML彻底的去理解。还是拆分成一个个ensures去理解的。
JML的好处就是在于可以把整个方法给限定住，可以很规范的把需求体现出来。但是经过尝试感觉相关的连接做的对新手不是很友好，大部分时间JML还是停留在类似于注释的阶段。
同时JML的书写由于需要离散数学的只是真的极度难读懂。对于一些副作用在涉及到数组的时候就开始奇怪了起来。
第四单元应该会更加注意随机数据的生成，并且多检查几次代码！避免手残（但我明明已经检查好几遍了。。。）