标签：抛出异常 错误 一键 做什么 简单 assign 方法 起点到终点 二次
以下内容来自我瞎翻译的维基百科：
JML是一种java的规约语言，使用了Hoare风格的前置，后置，和不变量约束条件，用来遵守契约式设计的要求。
这里面指出了JML的几个特点：
按照上面的介绍，可以明白JML可以分为 前置，后置，和不变量的要求，而具体描述则大致与数理逻辑的表达方式类似。
这些与数理逻辑类似的表达包括：
| \forall | 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。 |
| \exists | 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。 |
| \sum | 返回给定范围内的表达式的和。 |
| \product | 返回给定范围内的表达式的连乘结果。 |
| \max | 返回给定范围内的表达式的最大值。 |
| \min | 返回给定范围内的表达式的最小值。 |
| \num_of | 返回指定变量中满足相应条件的取值个数。 |
等，不再赘述。
其他描述也依据上面的分为三类
前置条件：是使用者需要满足的条件，若输入参数不满足该条件，则行为不可预测（你不仁，我不义）。基本的描述使用requires实现。
后置条件：保证执行结束后要满足的条件提示词为ensure
异常处理：抛出异常的要求。事实上，抛出异常也意味着一个方法的结束，可以看做一组特殊的前置——后置 规约。
signals (***Exception e) expr 当 expr 为 true 时，方法会抛出相应异常e。
signals_only (***Exception e) 满足前置条件抛出相应异常。
不变式：
assignable提示invariant进行规定其他关键词
\old指代方法执行前该量的值\result指代方法返回值工具链主要就是OpenJML的JML语法检查，以及JMLUnitNg实现的自动测试。
使用时将待测试的文件和Openjml.jar放在和测试代码一致的文件夹内，我选取了Person。
键入命令，可以看到：
所谓“没有消息就是好消息”，删掉了一个/*@pure*/,得到：
可以看到，OpenJML还是可以实现一些静态语法检查的。
参考诸位大佬（例如J）的博客,可以知道，大概执行以下四条命令就可以：
这里是我在win下用git bash的结果，前面的winpty是为了解决这样环境造成的显示错误，不重要。
winpty java -jar jmlunitng.jar src/Person.java
winpty javac -cp jmlunitng.jar src/*.java
winpty java -jar openjml.jar -rac src/Person.java
winpty java -cp jmlunitng.jar Person_JML_Test
然后就可以一条一条改报错了，开心。
前期听到他们解决不了/forall之类的，于是乎这些方法我先都删了。其次发现他的大意是，把JVM放在实现上方，于是魔改MyPerson，改名为Person并把规格都粘贴过去。
首先是第一条，如果你的JDK比8高，会得到：
（图片来源于水群，我的忘了截图）
然后是第三条,首先可以得到错误：
于是魔改Person，把private全换成public.
然后可以得到错误：
原来它不知道这个obj就是上一行那个啊，于是删掉equals。
之后，就可以喜迎：
挺好，总算到最后一条了。
这一条的问题其实不是JMLUnit的问题，是我的问题。注意到测试文件放在src下，而生成的Person_JML_Test.java也添加了：
package src;
理论上问题不大，包的路径和实际路径一致。
不过鉴于这里的分析，第四条反正要改成：
winpty java -cp jmlunitng.jar src.Person_JML_Test
就可以得到喜闻乐见的null，0,2147483647，-2147483648的结果了。
总之，这些工具年久失修，功能有限，在这方面，肯定比不上大佬们人工理解JML构造用例+随机大数据的测试结果了。
通过这次工具链实现，我熟练了gitbash的使用，清理了JDK8和JDK12打架的问题，还解决了命令行执行编译执行java的一些问题，受益匪浅。
其实三次作业的“设计架构”这个层面，感觉根本谈不上，毕竟我就是老师说的那种三个My选手（#此外还有一个简单Edge用来实现dij，后话）。这里只能谈一谈选取的设计结构和算法了。
第一次作业没什么好说的，基本就是JML复读，顶多就是把它用的静态数组换成Arraylist，另外value和Person的对应采取Hashmap.相应地，本次作业中的大量查询方法，由数据结构唯一确定。
使用Arraylist的方法，如acquaintaince相关的isLink(),就需要遍历来得到结论（这个其实也不必遍历，用value的containsKey()实现就行）。而value则可以直接由value.get()获取。
另外唯一需要“写”的方法，就是isCircle()方法，这里采取并查集实现，同时处于某些原因，没有进行路径压缩。
第二次作业的结果也可以看到，基本就是考虑时间，来思考如何选取数据结构和方法实现的问题。
第二次作业我在实现时，基本还是复读JML，只不过把新加入的数据结构做了一些处理：即，直接查询的全部使用HashMap或HashSet，需要遍历的就用ArrayList当碰巧两者都需要，那么就把数据存两份。
而实现的方法，我采取了动态更新totalage和tmp(getconflictsum()的结果)，这里是考虑到无论增删，他们的动态更新都方便实现。而其他方法完全复读，没有考虑真正复杂的\(O(n^2)\)的优化。
此外，增加了并查集的按秩合并和路径压缩。
在提交的时候，我不知道在做什么，忘了修改计划中的第一次作业中的低效查询和tmp的更新，导致死亡。
在这之后，更改了部分数据结构和实现：
增加了
HashMap<Integer, Person> idset;
优化getperson().
更改了isLink(),使用
value.containsKey(person);
此外，在计算relationsum 和valuesum时实时更新。
第三次作业数据结构没什么好说的，新增加的money要么作为MyPerson的field，要么拿一个HashMap存下来，写法和时间都差得不多。
而新增的delPerson()使得所有动态更新的值都需要增加逆运算，而它们的逆运算都显然且简单，所以也简单。
而连通块也很简单，其实无向图的isCricle()已经是每一个连通块了，而这些连通块用并查集已经全部求出来了。所以只要在维护并查集的时候顺便更新一下blocksum就好。
艰难的部分其实是queryMinPath和queryStrongLinked两个方法的实现（是算法和ds，我完了）。
而保证value为正则使得dijkstra成为普遍选择，且java有现成的PriorityQueue,不用自己手写堆，只要写个Edge类，实现compareTo()就可以了。而在具体实现过程中，其实还增加了一些更细致的判断条件：
isCircle()的时间复杂度更低，故而还是用isCircle()判断。另一点是关于queryStrongLinked的实现。这里的实现可以从几个角度来转化JVM的描述：
表示两点在同一个环上，于是采取dfs或bfs寻找环路。可以参考
注意到题目的要求其实是点双联通分量，采取相应的算法（比如讨论区那个我没完全搞定的）
注意到其实这里意味着从起点到终点的路上不经过割点。转而判断割点。而割点的判断可以从两个方面入手：
这里注意到了割点和连通块是可以相互转化的，所以可以不存割点，转而直接存下整个点连通块：
https://www.cnblogs.com/jiamian/p/11202189.html
这也是我事实上采取的方法。
此外，我也和dij一样，在关系不发生改变的情况下，先尝试从已经得到的BCC块里得到结果（这里是因为我在进行Tarjan的过程时，只遍历起点所在的连通块），如果失败，进行新的Tarjan的尝试。
这一个单元的学习，说实话难度没有很大。对我来说，最大的收获是在和同学讨论算法的时候，补上了自己数据结构的不少漏洞，学会了一些早就该会了的算法。
而JML作为一种形式化的规约描述，其实是一个非常理想化的浪漫工具：它一方面通过简单的对前置，后置，和不变量的限制，保证了程序运行的正确性。另一方面却也给方法的具体实现留出了足够大的自由空间。
此外，JUnit作为一种模块化测试工具，也拓展了我的测试手段，值得鼓励。
谈到这里，我这个单元由于第一次作业轻松通过，导致第二次作业时态度松懈，出现了一些纰漏，最后交了一个中期版本上去，死状惨烈。这也为我的轻视懈怠敲了一个警钟，让我能以更加谨慎的态度完成了第三次作业。
其实按照JML来写规格，对我来说，是比读文字参考书幸福太多的一件事情。
一方面得益于专门的形式化语言的结构比自然语言强太多（语法树都可以边去括号边画出来）。
另一方面也减少了很大一方面的思考量，就是如何把需求转化成相应的编程问题。这是我上一个单元要花时间思考的问题，即如何把需求转化成相应的设计模式，数据结构，和实现方法。这一单元很简单，只要读懂那几行JML描述，问题已经被分割得很细致了，不必再进行进一步的思考，思考已经不是“如何判断两个人是否认识”，而是直接去搜“如何求无向图的连通分量”。虽然助教们和老师仍然在强调“设计架构”，可是我眼中的设计，基本上就这样被削掉了一大半。
而且这样详细而细致的划分自然地带来了全局观念的不敏感，例如我至今也不知道题干的“关系网络”为什么要实现这些图论算法，尤其是minpath和stronglink(在得知value是好感度以后，越发不能理解)。
这也带来了我这次作业的一个问题：我根本没有意识到整体的层次架构。例如即使把“图论算法相关”分类出去，实际上也不过是把MyNetwork的部分field和method一键ctrl+X ,ctrl+V送出去，而我读到的代码，基本上也没什么所谓层次结构。
关于JML，像我前文所提到的定义来看，JML的两方面价值在于形式化和契约，形式化的很重要的一个特点是，它应该是没有歧义的，经过一些系列推导，甚至可以直接判断其完备性与否。然而这方面和oo相差甚远。我的感觉是，这件事只有写规格才能够有所体会。所以实验好评。
第二方面，就是它的契约，这事实上是单元测试十分重要的依据。例如第二次实验课，Junit的编写依据基本还是可以靠复读JML规格实现。这一点实际上还是很有意义的。可以看到，JUnit测试和JML的确很配。
谈到JUnit。
我在前两单元时曾经提过模块化测试的必要性，然而在第三单元第一次作业后，我满心欢喜地建了JUnit，却只是建立了而已。
当时的考虑大概如下：在本次作业除了我不熟悉的并查集以外，剩下的我靠读代码就基本能确保他们是没问题的了。而若是测试iscircle，它的数据量必然不小。既然那么多人都有了，还不如顺便把其他方法也测一测。此外，iscircle的JML是那种不可能直接拿来在JUnit复读的部分，所以还不如找个标程对拍。由于输出结果肯定会完全一致，所以反而比在JUnit写assertxxoo要省事。相比起前两个单元，反而这个单元对于单元测试的要求是偏低的。这里还是夸一下实验课，实验课对于JUnit的作用的体现对我来说比较明显。不过写Junit和读代码，也不一定哪个更快。
最后，这些JML工具链……
标签：抛出异常 错误 一键 做什么 简单 assign 方法 起点到终点 二次
原文地址：https://www.cnblogs.com/yukisshu/p/12934749.html
