标签：info 提高 生活 技术 cep 配置 度量 tab 返回
JML是JAVA Modeling Language的简称，主要用于对java程序进行规格化设计，是一种基于Larch方法构建的行为接口规格语言。
JML的优点在于它的精准性与可读性。在设计规格时，如果使用自然语言，那么很有可能会带有模糊性的描述，令代码实现人员感到困惑；而如果使用JML，那模糊的自然语言将被逻辑严密的规格语言代替，可以更好地表达设计思路。同时为代码书写规格，也可以提高代码的可读性，令其更好地被维护。
以下将对JML书写时使用的一些符号进行解释。
| 表达式 | 描述 |
|---|---|
| \result | 表示一个非void类型的方法执行后的返回值 |
| \old(expr) | 表示表达式expr在方法执行前的取值 |
| \not_assigned(x, y, ...) | 表示括号中元素在方法执行中是否被赋值，未赋值返回true，赋值返回false |
| \not_modifined(x, y, ...) | 与上一项内容基本相同，表示括号中元素在方法执行中取值是否变化 |
| \nonnullelements(container) | 表示对象container内部不会储存null对象 |
| \type(type) | 表示类型type对应的Class类型 |
| \typeof(expr) | 表示表达式expr对应的Class类型 |
其中\result与\old(expr)的使用频率较大，需要重点掌握。
| 表达式 | 描述 |
|---|---|
| \forall | 全称量词，表示对于给定范围的元素，每个元素都满足相应的约束 |
| \exist | 存在量词，表示对于给定范围的元素，至少存在一个元素满足相应的约束 |
| \sum | 返回给定范围内的表达式的和。例(\sum int i; 0 <= i && i < 10; i)表示0到9内自然数之和 |
| \product | 返回给定范围内的表达式的连乘结果 |
| \max | 返回给定范围内的表达式的最大值 |
| \min | 返回给定范围内的表达式的最小值 |
| \num_of | 返回指定变量中满足相应条件的取值个数 |
以上量化表达式都较为常见，尤其是全称量词与存在量词，二者的使用在规格描述中十分重要。
集合表达式
集合表达式个人并没有使用过。在这里只给出具体形式：new ST {T x|R(x)&&P(x)}即满足R与P约束的全部x变量。
操作符
操作符与java基本相同。但有增加子类型操作符、等价操作符、推理操作符与变量引用操作符。
方法规格
具体内容如下表：
| 名称 | 表示 | 描述 |
|---|---|---|
| 前置条件 | requires P | 调用者需要保证P为真 |
| 后置条件 | ensures P | 方法执行后的结果确保P为真 |
| 副作用限定范围 | assignable、modifiable | 方法在执行过程中会修改对象的属性数据或是类的静态成员数据 |
同时还有一些其他的关键字，如pure代表纯粹的访问性方法，normal_behavior与exceptional_behavior区分正常行为与异常行为，signals字句与signals_only字句用以抛出异常等等。
OpenJML
OpenJML的基本功能就是对JML注释的完整性进行检查。大致有类型检查、变量可见性检查、变量可写性检查。可以使用相应的命令行进行操作。具体可到http://www.openjml.org进行下载。
JMLUnitNG
其基本功能是根据JML规格生成对应的测试样例以确定代码的正确性。具体可到http://insttech.secretninjaformalmethods.org/software/jmlunitng/下载
Junit
自行构造数据，对代码进行验证。只需要在项目中添加两个jar包，使用方式较为简单，容易上手，是以上三种工具中个人常用的一种。
下载junit.jar : https://repo1.maven.org/maven2/junit/junit/4.13/
下载hamcrest-core.jar : https://repo1.maven.org/maven2/org/hamcrest/hamcrest-core/1.3/
关于OpenJML，个人下载了具体的工具。但是确实不会使用，报错信息一大堆。个人先改了jdk，又改了环境变量。但是还要合成Person与MyPerson，修改JML。因此个人还是放弃了，确实难以使用这个工具。
最后个人魔改了Person进行尝试，但还是无果，遂放弃。
对于这个工具，个人有进行一定的尝试，但确实使用不来。因此个人决定按照讨论区的内容魔改并简化group以完成测试。
根据讨论区内容，魔改group与person，将其加入test文件夹，之后还要依次输入以下4指令：
java -jar jmlunitng.jar test/Group.java
javac -cp jmlunitng.jar test/*.java
java -jar openjml.jar -rac test/Group.java test/Person.java
java -cp jmlunitng.jar test.Group_JML_Test
但最后还是有问题，无法得到有效的结果。个人确实是不会使用这个工具吧。
关于其生成的样例，个人查看了舍友的结果。个人感觉生成的样例强度并不高，一般都是测试null或是边界值的样例，缺乏代表性。
相比这样自动生成的样例，我认为使用Junit更能测试代码的正确性。
本单元三次作业的架构大致相同，更多的区别还是在于方法实现上。
第一次作业UML类图、相关度量分析如下：
第一次作业的难度并不高，但也确实是第一次接触JML，因此第一次作业基本是按照JML规格去写代码。这样的效率确实不高，如果测试时想卡也确实可以。同时第一次作业的结构也是最为简单的，只要认真阅读jml规格，应该都是没有问题的。唯一一个可能有问题的方法就是isCircle，查询两点是否连通。此时最好不要使用dfs，从运行时间和所占内存来看，这都不是一个好选择。使用bfs可以在时间和性能上都甩开dfs，使用并查集也同样。
第二次作业的UML类图、相关度量分析如下：
第二次作业相比于第一次作业，增加了Group接口，且大幅增加Network里的方法。在测试上，测试的指令条数也有了一个数量级的增长。
因此，在第二次作业中，个人修改了大量的访问方法。如根据id查Person、Group、value等等，个人之前选择的是遍历方法，但根据第二次作业测试的指令数来看，这一定会ctle。因此，个人设置了大量的hashmap来储存各项数据间的对应关系（利用id的唯一性）。但是第二次作业还是出现了一些问题，即使使用了hashmap，还是有个别测试点ctle，具体情况在下一部分bug与修复介绍。
第三次作业的UML类图、相关度量分析如下：
第三次作业相比于第二次作业有很大的不同，最主要的还是函数三大难。
同时第三次作业，个人还实现了缓存以增快访问速度。缓存大多数处于MyGroup类中，储存当前Group中成员的年龄和、年龄平方和、关系总数、value和、冲突情况等等。
第一次作业较为简单，没有出现bug，因此在这里不予赘述。
第二次作业出现了问题，主要是ctle，即cpu的运行时间过长。为解决此问题，个人引进了缓存机制。
原先对于MyGroup中的求方差、求均值、求value和等等方法，个人都会采用遍历的方法。都是对求value和、关系数和等等时，将进行二重循环，此时的时间复杂度会很高。因此个人打算改为缓存机制，记录以上的特殊值，大致有年龄和、年龄平方和、关系总数、value和、冲突情况等等。每次添加人进入group时需要更新相关数据，添加关系时要更新全部group的值。
第三次作业没有过大的问题，唯一的问题在于个人的粗心大意，在borrowMoney中加减符号出现了问题。本来这个问题是可能会导致强侧一片wrong answer的，但强侧似乎没有这个考察点，因此个人逃过一劫。但还是在互测时被同学发现。
本单元我们学习了JML规格。但大多数时候，我们还是在看规格写代码，在写规格上的练习还是太少（实验有涉及部分）。我认为我们应该在这一部分加强训练，这样才能在设计时给出合乎规范的规格。
JML规格可以在我们设计构思时起到重要作用，它可以帮助我们向他人传递自己的想法，并且可以做到逻辑严密，不会产生模糊的定义。并且我们也可以通过JML规格更好地阅读他人的代码、理解他人的构思。这在工程项目的多人协作中是十分重要、十分有意义的。
对于JML的工具链，个人觉得很是鸡肋。OpenJmL的各种事情实在太多，不好使用。个人在配置时换了jdk，改了路径，还要变更代码，最后还是出了很多不知名的bug，可能确实是个人能力有限使用不了吧。对于JMLUnitNG，它的使用也很麻烦，测试使用的样例也只是一些边界条件，和个人手撸没有太大的区别。
唯一一个让我感到还不错的的工具是Junit，这个工具的配置并不复杂，也没有什么过多的约束。因此个人的一些测试都是使用工具Junit，这也算是一个不错的收获。
总结一下，这个单元还是有很大的收获。虽然以后可能用不到JML，但它的思想是非常有意义的，这对我们以后的学习、生活以及工作，都可以产生不小的影响。
标签：info 提高 生活 技术 cep 配置 度量 tab 返回
原文地址：https://www.cnblogs.com/lukx21/p/12940512.html
