标签：floyd算法 并且 语法检查 type mamicode 计算 定义 最小值 person
\result表示非void类型的方法执行所获得的结果，即方法执行后的返回值。
\old(expr)用来表示一个表达式 expr 在相应方法执行前的取值。
\not_assigned(x,y,...)用来表示括号中的变量是否在方法执行过程中被赋值。
如果没有被赋值，返回为true，否则返回 false,主要用于后置条件的约束表示上.
\not_modified(x,y,...)与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
\nonnullelements(container)表示container对象中存储的对象不会有null
\type(type)返回类型type对应的类型
\typeof(expr)返回expr对应的准确类型。
\forall 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum 返回给定范围内的表达式的和。
\product 返回给定范围内的表达式的连乘结果。
\max 返回给定范围内的表达式的最大值。
\min 返回给定范围内的表达式的最小值。
\num_of 返回指定变量中满足相应条件的取值个数。
JML表达式中可以正常使用Java语言所定义的操作符，包括算术操作符、逻辑预算操作符等。此外，JML 专门又定义了如下四类操作符。
子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如果E1和E2是相同的类型，该表达式的结果也为真
等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2
推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1
变量引用操作符：\nothing指示一个空集；\everything指示一个全集，即包括当前作用域下能够访问到的所有变量。
前置条件：使用requires子句，意思是确保后面的条件为真。可以有多个requires子句，表示并列关系。
后置条件：使用ensures子句，确保方法执行返回结果满足条件的要求。同样也可以有多个ensures子句，表示并列。
副作用：使用assignable或者modifiable。Assignable表示可复制，modifiable表示可修改，大部分情况可以交换使用。
不变式invariant，要求在所有可见状态下都满足。
状态变化约束constraint对前序可见状态和当前可见状态进行约束。
我尝试使用了OpenJML还有JMLUnitNG，JUnit。
OpenJML可以对规格进行语法检查，JMLUnitNG可以生成测试样例，之前用来跑了一下简单的程序，发现它只是生成了几个边界数据构成的样例。JUnit可以进行单元测试，并通过JUnit找到了一个bug。
java -jar .\openjml\openjml.jar -exec .\openjml\Solvers-windows\z3-4.7.1.exe -esc .\homework\unit3\task2\src\com\oocourse\spec2\main\Person.java
对官方接口的Person类进行检查，检查通过
在里面将\result中的”\”删掉，报了下面的错误
看了讨论区大佬的博客，将Person作了修改，并且使用下面四条指令完成了测试样例的生成
java -jar jmlunitng.jar test\Group.java
javac -cp jmlunitng.jar test\*.java
java -jar openjml\openjml.jar -rac test\Group.java test\Person.java
java -cp jmlunitng.jar test.Group_JML_Test
从测试结果来看，addPerson和hasPerson对于参数为null的情况都发生了错误，在编写程序时没有考虑到参数为null的情况，这是因为在评测时不会产生null的对象。（updateSum是自己编写的方法，对于边界数据会发生溢出，这里不做分析）
从测试数据来看，JMLUnitNG生成的测试样例主要都是null，0以及int可以表示的最大值和最小值，只是测试边界情况，不能进行覆盖性的测试。
第一次作业：
基本是按照JML规格，直接进行翻译来实现。
在Person中使用HashMap来映射Person和Person对应的value值。
在Network中使用BFS来进行isCircle的判断。
第二次作业：
首先将第一次作业做了一定的改动，在Network中使用并查集来判断isCircle。查询平均数和方差都使用了变量存储value的和，value的平方和，在查询时，使用这两个变量进行平均数和方差的计算。其余新增方法基本都直接按照JML规格进行翻译。
第三次作业：
这次的三个函数难度都有些大，我在写之前查找了很长时间的资料，最终找到了合适的算法实现。
最短路算法使用堆优化的dijkstra，当时考虑过使用floyd算法，但是复杂度有O(n^3)，优化的方法是设置缓存，一种是设置dirty，在两次查询中的间隔又增加新的关系，就重新计算。另一种是在增加新关系的过程中维护最短距离数组，在知网上查找到一篇相关论文《网络中两结点之间增加一条弧后的最短路校正算法_雷治军》，里面对数据的修正也需要O(n^2)的复杂度，对于少量查询的情况时，这样显然不够划算。所以最终我还是采用了dijkstra算法。
Stronglinked则使用了tarjan算法，似乎效率最高并且比较好写的就是tarjan算法了，以id1为源点搜索所有点双连通分量，每当完成一个双连通分量的搜索，就查看分量中是否含有id2所对应的点，若查找到，则将flag设置为true，并且返回。
连通块数则借助并查集来实现，通过遍历所有Person，使用findfa方法找到他们的根节点，使用HashSet存储，最后只需要返回HashSet的大小就可以。
整体上来看，使用HashMap表示id和value（MyPerson中），id和group（MyNetwoek中），能够较快的完成对id的索引。对于第三次作业的图的相关算法，使用HashMap将每个MyPerson映射到一个整数。用整数来表示每一个Person，方便使用ArrayList<Vector>来建立邻接表，Vector存储第i个节点的邻接节点，这样省去了对Person的查询操作。
第一次和第三次作业强测全部通过，第二次作业发生了几个致命的错误导致所有点都没有通过。
第一个错误是忽视了Group中size为0时，平均值和方差都应该为0的情况，导致了除0异常。第二个错误是使用HashMap时，错误地使用contains方法去判断是否含有key，这种情况在第一次作业中检查出来了，但第二次写的时候又忘记了。
在中测阶段，只有第三次作业使用了Junit，并且我对几个新增方法做了一些测试，其中有一个方法测试未通过。通过检查发现错误并不是新增方法导致的，结果意外地发现了第二次作业的一个遗留bug，最终强测满分通过了。
从面向对象这门课，我学到了很多的设计思想。JML让我体验到了契约化设计，通过保证前置条件，后置条件，副作用还有不变式和约束，在满足规格的前提下，这段代码对于规格来说，就是正确的。也让我意识到，在构思一个Project时，先不用着急去实现具体的代码，可以通过书写规格来完成对代码的形式化设计，规格将设计与实现分离，这样能够更好的保证程序的正确性，同时也方便了我们使用Junit等工具展开测试。
本单元是我对程序整体架构感到最清晰的一次。对于前两次作业，我中测提交的代码基本都是直接对照规格进行翻译，第一次作业倒是没有问题，然而第二次在强测中出现了CTLE的情况。让我明白规格只是给出一种形式化的表述。在满足规格的情况下，我们还需要寻找性能更好的实现方式，更好的性能依赖于算法。为了保证正确性，也要做好测试。
既然规格不涉及具体实现方式，希望以后可以有按照规格验证代码正确性的工具，希望从更抽象的角度去解决问题。我会在以后的程序设计中，尽量会使用规格去完成设计，然后再去实现，同时使用Junit进行相应的测试。
标签：floyd算法 并且 语法检查 type mamicode 计算 定义 最小值 person
原文地址：https://www.cnblogs.com/l-cg/p/12944072.html
