标签：OO 总结 java jar Person 规格 单元 使用 表达式
OO第三单元总结
一、 JML语言的理论基础及应用工具链
（1）JML语言理论基础
1.原子表达式：
\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对应的准确类型。
2.量化表达式
\forall 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum 返回给定范围内的表达式的和。
\product 返回给定范围内的表达式的连乘结果。
\max 返回给定范围内的表达式的最大值。
\min 返回给定范围内的表达式的最小值。
\num_of 返回指定变量中满足相应条件的取值个数。
3.操作符
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指示一个全集，即包括当前作用域下能够访问到的所有变量。
4.方法规格
前置条件：使用requires子句，意思是确保后面的条件为真。可以有多个requires子句，表示并列关系。
后置条件：使用ensures子句，确保方法执行返回结果满足条件的要求。同样也可以有多个ensures子句，表示并列。
副作用：使用assignable或者modifiable。Assignable表示可复制，modifiable表示可修改，大部分情况可以交换使用。
5.类型规格
不变式invariant，要求在所有可见状态下都满足。
状态变化约束constraint对前序可见状态和当前可见状态进行约束。
（2）应用工具链
我尝试使用了OpenJML还有JMLUnitNG，JUnit。
OpenJML可以对规格进行语法检查，JMLUnitNG可以生成测试样例，之前用来跑了一下简单的程序，发现它只是生成了几个边界数据构成的样例。JUnit可以进行单元测试，并通过JUnit找到了一个bug。
二、 部署使用SMT Solver,JMLUnitNG
1.使用OpenJML的Solver
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中的”\”删掉，报了下面的错误
2.使用JMLUnitNG
看了讨论区大佬的博客，将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的查询操作。
四、 Bug和修复情况
第一次和第三次作业强测全部通过，第二次作业发生了几个致命的错误导致所有点都没有通过。
第一个错误是忽视了Group中size为0时，平均值和方差都应该为0的情况，导致了除0异常。第二个错误是使用HashMap时，错误地使用contains方法去判断是否含有key，这种情况在第一次作业中检查出来了，但第二次写的时候又忘记了。
在中测阶段，只有第三次作业使用了Junit，并且我对几个新增方法做了一些测试，其中有一个方法测试未通过。通过检查发现错误并不是新增方法导致的，结果意外地发现了第二次作业的一个遗留bug，最终强测满分通过了。
五、 心得体会
从面向对象这门课，我学到了很多的设计思想。JML让我体验到了契约化设计，通过保证前置条件，后置条件，副作用还有不变式和约束，在满足规格的前提下，这段代码对于规格来说，就是正确的。也让我意识到，在构思一个Project时，先不用着急去实现具体的代码，可以通过书写规格来完成对代码的形式化设计，规格将设计与实现分离，这样能够更好的保证程序的正确性，同时也方便了我们使用Junit等工具展开测试。
本单元是我对程序整体架构感到最清晰的一次。对于前两次作业，我中测提交的代码基本都是直接对照规格进行翻译，第一次作业倒是没有问题，然而第二次在强测中出现了CTLE的情况。让我明白规格只是给出一种形式化的表述。在满足规格的情况下，我们还需要寻找性能更好的实现方式，更好的性能依赖于算法。为了保证正确性，也要做好测试。
既然规格不涉及具体实现方式，希望以后可以有按照规格验证代码正确性的工具，希望从更抽象的角度去解决问题。我会在以后的程序设计中，尽量会使用规格去完成设计，然后再去实现，同时使用Junit进行相应的测试。
标签：OO,总结,java,jar,Person,规格,单元,使用,表达式 来源： https://www.cnblogs.com/l-cg/p/12944072.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。