标签：参数 资料 过程 str ash inf exce jks 方式
第三单元主要考察的是对JML的理解以及根据JML提供的相关信息来设计的能力，当然，这里对一些算法的考察，好像又梦回数据结构（数据结构没学好的哭了
JML就是The Java Modeling Language，顾名思义，也就是为了让程序有个既定的规格，让我们补全类中的参数以及所含方法时有迹可循，即不至于看不懂这个光秃秃的父类是用来干嘛的，根据JML规格中的信息，我们可以了解到这个类需要包含的数据，也可以知道方法的正常情况以及异常情况下的操作等，实现了规格设计者与代码完善者的良好沟通。
首先，JML以javadoc注释的方式来表示规格，每行都以@起头，有两种注释的形式，一种是行注释，即//@xxx，还有一种是块注释，即/*@xxx @*/，一般规格就一行可以解决的时候，使用第一种，如果比较复杂，则使用第二种。对类中所需包含的数据的规格一般直接紧跟在Class xxx下面，而对方法规格的描述一般紧挨着方法的声明，位于方法上面，如图所示。
图1
如上图，规格中写的non_null Person[],表示我们要确保这个数组不为null，这一句规格就说明了我们要设置一个元素为Person的数组people。
再看方法的规格，
requires子句表示的是这个方法应满足的前置条件，如果这个都无法满足，那么结果是不正确的；
ensures子句表示的是这个方法的后置条件，即满足了前置条件的话，方法执行完之后的返回值或者结果也相应地应满足的条件；
assignable后跟的东西表示的是副作用，也就是方法执行过程中会改变的东西，常见的是跟着\nothing，也就是什么都不改变。
不改变任何东西的方法，比如一些查询所含元素内容的方法，都是pure的，也就是图中用/*@pure*/修饰的。
（需要注意的是：规格中每个子句都应该以分号结尾！！！否则JML工具会无法解析！）
图二
normal_behavior表示的是正常操作，也就是在这个前提条件下，进行操作是正常的；
相应的，有exceptional_behavior，它表示的是异常情况，在满足某个前提条件下的操作是异常的。
异常情况需要抛出异常，那么抛出什么类型的异常呢？用signals（xxx）语句，括号里即为所需抛出的异常类型，语句后面为判断为异常情况需满足的前提条件。
在图中，我们还经常看到also，因为不止一种前提条件的时候，会有多个不同的normal或者exception的情况，那么他们之间就可用also来连接。
我们学过离散数学，还记得大一的时候有一段痛苦的经历里，经常出现的全称量词和存在量词，在JML他们分别为 \forall，\exists，他们的形式一般都是（\forall int x; ; ），量词后面紧跟的是修饰的变量，那么就是在后面所规定的范围内，所有变量都得满足或者存在至少一个变量满足所给出的条件。
与这两个量词类似，还有一个\sum，也经常用到，是对相应范围内，满足条件时候，对所需求和的东西求和。
要基本看懂JML的规格，还有一点内容没说到：
\nothing表示没有东西，\old（xxx）表示的是括号里的东西改变前的状态，\result表示的是方法执行的结果（一般是返回值）。
好了，知道了上面的基本知识，再根据某些地方的伪代码，加上自己的理解，就可以基本读懂很多JML了，当然，也会有很长...很长...很长的、很难...很难...很难理解的，那就只能稳住心态慢慢看了...
可能只有我们学校的计算机系才学这个？？相关资料感觉并不是很多很好，而且这几个工具链....相信想吐槽的不只是我一个人，就是各种报错，各种跑不起来，也可能因为我太菜了，所以跑不起来...就说一说我能跑起来的吧...
首先是课程中无论是作业还是实验都要求使用的Junit，Junit是用来对我们写了JML的程序进行单元测试的，但是这个单元测试还是挺...挺需要耗费时间精力的，可能有其他的方法测试，但是我都是手撸一些数据（也造不出什么很np的数据来搞），然后测试要那个覆盖率，也需要多一些边界条件的测试。
然后是写这次博客需要使用的SMT Solver，这玩意儿确实有点儿坑，部署open_jml是个问题，然后各种报错，各种问题，最后重新写了一下类，才勉强跑起来，需要注意的是：需要用jdk8！！
最后是JMLUnitNG，也比较难以使用，但是可以进行随机测试，虽然覆盖率较差，在某种意义上，还是挺有好处的。
理清了用JML写规格的基本知识后，第一次作业可以基本按照规格来写，就是完成三个类的实现，主类以及MyPerson, MyNetwork类，他们要借助于给我们的接口来实现，注意异常情况的抛出即可，但是第一次作业有一个比较难写的方法，就是isCircle（）方法，这是这个单元开始浮现数据结构阴影的缩影。
图三
这个方法其实就是查询有没有从id为id1的人到id为id2的人的路径，这里我使用的是dfs，写好了这个方法基本上可以进互测，强测也不会有太大问题。（当然，这一单元出bug的话，不要死盯着dfs，就是isCircle这个方法去看，因为也许错误出现在其他的地方，有的时候“眼瞎、手残“照着JML写都可能会写错的...
第二次作业是真正让我们理解到这单元中测是烟雾弹的一次作业，中测就加了个Group的接口，看JML规格也比较简单，没有什么很难实现的地方，结果有些人（包括我... 就掉以轻心，这第二次作业确实是迭代，怎么加的东西这么少，感觉难度没啥上升啊，反而比第一次还更简单，没什么难实现的方法，结果莽上去，强测爆0，或者一丢丢分，全TLE了....
到这里才知道，不能哪儿都图个便捷使用arraylist，因为第二次作业数据量很大，而且有大量的查找等操作，那么使用hashmap这个结构是比较合适的，把该使用hashmap的地方改过来，应该就问题不大了，还有同学讨论了hashmap和arraylist的设置其初始大小的问题，应该可以直接设置一个比较大的空间，用空间换时间，减少后期它自动扩容的时间。
这是我第二次作业的一些复杂度的分析，看上去还是八太行，有好多地方需要改进的，那么如果你也比较懒的话，就把这个锅留给第三次作业吧...
第三次作业并没有新增什么类啊接口啊，但是network接口里新增了很多方法，还有好几个不好写的，这下难度一下就上去了，关键是那些算法与数据结构有关，没学好的得赶紧去恶补一下这里用到的知识，这里主要有几个方法里用到了Dijkstra算法，而且还是堆优化的，然后还有bfs、并查集等的使用，反正就难度上去了，我这种不会算法的就凉了...
一切的困难得从queryMinPath（）说起，这个方法规格中写到需要调用isCircle（），还要进行其他操作，那么这复杂度肯定就上去了，这就是最短路径的算法，我们会想到使用Dijkstra算法，但是你以为写出来就万事大吉了？有同学分析了复杂度，发现光秃秃的Dijkstra算法大概率被卡，那么就还需要加上堆优化，这就更加增添了对我们的要求以及题目的难度...
然后是queryStrongLinked（）这个方法，通过对规格的分析相信很多人一开始都想使用两次bfs或者说两次dfs，但是这种方法同样被大佬否定了，因为他们举出了反例，这样的话，我们就被迫采用其他正确、且复杂度不是很高的算法来解决问题。
最后是queryBlockSum（）方法，这个方法如果不使用并查集的话，就直接暴力应该是会超时的，那么我们就得去学习一下并查集的知识，有一篇“江湖门派”的帖子挺好的，推荐一手。
JML写出的规格虽然很清晰，但是我们不可以直接按照里面给的思路去写，还得经过自己的思考，加以辨别筛选，选择比较好的架构以及数据结构去写代码，不然光是跟着JML去写，肯定是无法通过测试的，然后我们也学到了要自己多进行测试，以前就拿评测机作为测试工具的人这次就吃了大亏，以为中测过了就万事大吉，其实只是个烟雾弹，狠的在后面！！还是不可以掉以轻心！
标签：参数 资料 过程 str ash inf exce jks 方式
原文地址：https://www.cnblogs.com/wxrspig/p/12938799.html
