其他分享
首页 > 其他分享> > OO第三单元总结-JML

OO第三单元总结-JML

作者：互联网

OO第三单元总结-JML

JML理论基础

1.定义：

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。JML可以用于开展规格化设计和提升代码可维护性。

2.常见用法：

/*@ public normal_behavior        			//表示正常行为

      @ requires !(\exists int i; 0 <= i && i < people.length; people[i].equals(person));       		//前置条件，在people容器中不存在person时。
      
      @ assignable people, money;  		//people和money两个变量可以被修改
      
      @ ensures people.length == \old(people.length) + 1;   //people容器大小加1
      
      @ ensures money.length == people.length;   //money大小等于people大小
      
      @ ensures (\forall int i; 0 <= i && i < \old(people.length); 
      @         (\exists int j; 0 <= j && j < people.length; 
      @         people[j] == \old(people[i]) && money[j] == \old(money[i])));
      //后置条件，对任意的一个在原来people容器中的person，都在新的people容器中存在一个对应，且money也对应。
      
      @ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person && money[i] == 0); //后置条件，表示在新的容器中存在person，且其对应的money为0
      
      @ also
      @ public exceptional_behavior //表示异常行为
      
      @ signals (EqualPersonIdException e) (\exists int i; 0 <= i && i < people.length; people[i].equals(person));  //signal子句，表示在people已经存在person时抛出异常。
      @*/

3.JML应用工具链：

OpenJML：使用OpenJML可以对JML代码实现静态语法检查和运行时检查。
JMLUnitNG：根据JML语言自动生成TestNG测试文件检查代码正确性。
JMLUnit：根据JML语言构造测试方法和测试用例，检查相应JML规格和代码实现的正确性。

从上面的测试样例可以看出，这个测试只是对边界情况进行了一些考虑，感觉这种方法还不如Junit以及对拍香，我更愿意选择对拍以及自动化测试进行验证，这个工具对极端情况还是能够做一个较好的分析。但是总体来说真的不知道这个有什么用处，极端情况的测试也并不完全。以上代码fail的都是因为不存在的情况。

作业分析

第一次作业：

本次作业没有什么难点，主要是熟悉JML语言，根据JML语言的语义进行实现就行，本次较为复杂的一个方法时iscircle，我采用了并查集的算法，时间复杂度较好。没有对架构采取什么改变，就是在原有的接口上实现自己的算法即可。

第二次作业：

在第一次作业的基础上加上了一个Group类，Group类的难点主要是在getRelationsum，getValue，getAgeMean，getAgeVar，这几个方法上，以getRelationsum和getAgeMean为例。（需要仔细阅读JML规格，搞清楚for循环到底是对那些进行遍历）
对于getRelationsum，这个值的改变只会在人加入group和加关系的时候，所以只用通过这两种情况进行考虑即可实现。
对于getAgeMean，可以用一个agesum来缓存当前group中所有人的age和，这样的话就可以实现O(1)询问。

第三次作业：

本次作业的难点主要是要知道两个新的算法，tarjan实现点双连通分量以及dij堆优化算法，主要的难点在于stronglink需要寻找点双连通分量，以及minpath找两个点的最小距离，还有qbs寻找当前连通块的个数（直接通过并查集O(n)实现）。
本次作业新加了一些类，主要是对图的数据进行管理，为了让代码更好看以及符合面向对象的要求。下附第三次作业的架构图：

BUG分析

在这个单元的三次作业中，在第二作业中出现了一个小的BUG，即对规格中没有出现的情况的处理，本以为测试数据不会出现不满足requires的情况，并且以为测试的时候也不会超出requires的情况，但是在本单元的作业中，没有出现=直接return，导致出现了一个BUG。
本单元的hack，都是通过阅读代码进行hack，这也许就是JML的一个好处，因为都是实现同一个接口，所以大家的方法都大同小异，并且可读性较强，本单元仅在第二次作业的时候hack成功，主要错误是iscircle采用了暴力DFS算法，导致了TLE，还有就是对于getAgeMean的规格化描述理解的偏差，以及除0的错误。

心得体会

这个单元主要是学习了一种规格化的方法，JML语言主要就是对方法进行规格化描述，不仅仅方便了使用者也方便了实现者，并且通过此次的互测，我更加深刻的理解到了JML语言的好处，就是可以方便debug，可以清楚的知道架构，就可以更好的定位错误。
在这个单元的学习中，总感觉有点不那么OO，主要是因为第一二单元的体验极好，体会到了设计模式的重要性，以及线程安全的重要性，并且都是自己从头进行编程，可以训练架构以及对于OO各种原则的训练，对类的构建以及类的解耦等都有着很大的提升，感觉第三单元只是对JML语言的了解以及算法的了解，但是总体来说对于规格化的思想有了一定的了解，也是一种不一样的体验。
最后希望OO课程可以办的越来越好，希望能够更加OO。

标签：OO,JML,2147483647,addRelation,Passed,2147483648,null,单元
来源： https://www.cnblogs.com/zhy123/p/12939419.html