标签：访问 产生 ons require ase heat get 推理 length
Tags: OO
JML是一种用于形式化表述程序规格的语言，其具体实现方法是通过逻辑推理语言对程序的输入输出以及数据交互做出限制，来保证程序按照设计者的预期运行。同时它也被用来提高代码的可维护性和可读性，通过针对已有的代码写出其JML规格，有利于维护该代码。
在本文中，并不会照搬课程组所给的JML教程来对JML进行讲解，本文的目的，在于表述笔者在完成三次作业中对JML规格的体会。
JML规格可以粗略的分为两种，类的基本属性的规格和类的方法的规格。
JML可以规定一个类应该具有什么属性域，比如具有某个数组，某个用来计数的整型变量等等，我们可以把作业中的network中有关的JML拿来当作一个例子：
public interface Network {
/*@ public instance model non_null Person[] people;
@ public instance model non_null Group[] groups;
@ public instance model non_null Message[] messages;
@ public instance model non_null int[] emojiIdList;
@ public instance model non_null int[] emojiHeatList;
@*/
从上面的代码我们可以看出，Network这个类要求有五个数组，实际上，说它们是数组并不是意味着我们实现规格的时候真的把它们为它们申请数组空间，相反，我们可以把它们申请成为链表甚至是哈希表，因为这里的数组只是用于后续的规格表述之中，我们后面可以看到为什么在规格表述的最开始把它们定义为数组有利于后续为方法写出规格。
JML对方法规格的表述一般有以下几个方面：前置条件，对类的属性域的修改限制，对方法调用后副作用的限制，对返回值的限制，对异常行为的规定。我们一个一个来说。
前置条件是对方法运行前进行判断，根据当前属性域的值，决定方法如何执行，具体可以看下面一个例子：
/*@ public normal_behavior
@ requires contains(id);
@ ensures (\exists int i; 0 <= i && i < people.length; people[i].getId() == id &&
@ \result == people[i]);
@ also
@ public normal_behavior
@ requires !contains(id);
@ ensures \result == null;
@*/
public /*@pure@*/ Person getPerson(int id);
上面的JML语句中规定了在两种不同条件下方法的返回值。
JML中通过关键字assignable来说明该方法会对那些属性域进行修改，而有时希望方法的执行对某些属性域没有影响，就会使用作用符\not_assign来作说明。
这个关键会被用来说明方法执行后产生的作用，例如我们要求某个方法删去了数组里某个特定的对象，那么就可以用这个方法来对数组进行限制，要求方法执行后数组中不存在该元素。可以看下面的一个例子：
/*@ public normal_behavior
@ requires !(\exists int i; 0 <= i && i < people.length; people[i].equals(person));
@ assignable people;
@ ensures people.length == \old(people.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(people.length);
@ (\exists int j; 0 <= j && j < people.length; people[j] == (\old(people[i]))));
@ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person);
@ also
@ public exceptional_behavior
@ signals (EqualPersonIdException e) (\exists int i; 0 <= i && i < people.length;
@ people[i].equals(person));
@*/
public void addPerson(Person person) throws EqualPersonIdException;
这是向people这个数组中添加元素的一个方法，我们可以看到，如果执行方法时属性域满足第一个requires后面的表达式，那么方法执行后需要满足三个ensures后的表达式，这三个分别说明了：
在上面的例子中，我们还可以注意到有一个关键字signals，它的作用就是在某些条件下要求方法抛出规定的异常，这里的“某些条件”就是所抛出异常后紧跟的表达式。
编写为每个方法编写测试类进行单元测试，下面为对MyNetwork类中的contains方法写的单元测试代码：
import com.oocourse.spec3.exceptions.EqualPersonIdException;
import junit.framework.TestCase;
public class MyNetworkTest extends TestCase {
MyNetwork myNetwork = new MyNetwork();
public void testContains() throws EqualPersonIdException {
myNetwork.addPerson(new MyPerson(1, "a", 1));
assertTrue(myNetwork.contains(1));
assertTrue(myNetwork.contains(0));
}
}
通过单元测试的方法可以对方法实现逐个测试，实现迭代开发。
这种方法的优点是测试单个接口起来十分简单，易于理解，缺点是对于每个方法都需要单独写一个测试方法，测试代码数量与待测试方法数成正比。
抱紧jxm同学的大腿，他已经为我们写好了测评机并改进了随机数据生成器，通过构造的数据来对多位同学的代码进行对拍查看是否存在bug。
纯随机生成数据进行测试的效率很低，因此为了提高效率，需要限制出现的id的范围等等，使得代码覆盖率提高到一个可以接受的范围。
测评机和数据生成器都是通过C代码写成的，C代码通过调用命令行接口来运行每份参与对拍的代码，获得运行结果，再通过系统调用来进行文本比较，得到评测结果。
这种方法的好处在于不需要编写繁多的测试方法，通过文本比对就能知道对拍的代码中是否有bug。坏处在于，无法定位bug的来源，甚至无法知道通过对拍的代码是否还有正确性的问题。
hashtable是我非常喜欢用的一个容器类，学过数据结构的我们知道，hashtable兼具了数组和链表的优点和缺点，是两者的一种trade-off，通过它，我们可以在时间和空间上取得较好的协调。
在我的作业中，我对所有有id的信息的集合都使用了hashtable来加快查找，比如person、message等。
HashSet也是用来加快查找的一种容器类，由于Network中的isCircle方法需要采用并查集算法来改进时间复杂度，所以利用到了HashSet来作为集合使用，值得注意的是，本单元的作业所给的空间都比较充裕，所以这里大量的使用了空间换时间的思想来加速程序。
PriorityQueue，也就是优先队列，被用来加速dijstra算法，通过它，我们就不需要以O(N)的复杂度在待访问的点里找到权重最低的那个点，复杂度降低到了O(1),这样，dijstra算法就不会成为时间的瓶颈，在最后一次作业里，我们看到强测结果很不错，说明优化的方向是正确的。
容器类的选择，本质上是对数据结构的选private final Hashtable<Integer, HashSet
private int blockSize = 0;择，细节上这是对Java底层实现原理的了解，最后还有对程序运行的时间和空间条件的trade-off，把握住了这三个方面，容器类的选择与使用便不再是难题了。
本单元我的性能问题，主要出现在连通块的判断上，在第二次作业中TLE了两个点，究其原因在于，代码统计连通块的复杂度为O(N),经过优化之后，复杂度降低为O(1)。下面简要描述一下我的实现过程。
首先对于每个加入Network的person对象，它们在图网络中最开始都是一个孤立的点，所以连通块要加一，当我们向Network中加入一个关系时就相当于加入了一条边，如果被相连的两个点本来不连通，那么现在连通块的块数减一，同时将这两个点放入同一个连通块的集合里，否则什么也不做。
具体的数据结构是：
private final Hashtable<Integer, HashSet<Integer>> blockTable = new Hashtable<>();
private int blockSize = 0;
其中blockTable就是“并查集”。
本单元最主要的架构设计集中在MyNetwork这个类里，为此而外定义了许多数据结构来加速查询，具体如下：
public class MyNetwork implements Network {
private final Hashtable<Integer, Person> personTable = new Hashtable<>();
private final Hashtable<Integer, HashSet<Integer>> blockTable = new Hashtable<>();
private int blockSize = 0;
private final Hashtable<Integer, Group> groupHashtable = new Hashtable<>();
private final Hashtable<Integer, Message> messages = new Hashtable<>();
private final Hashtable<Integer, Hashtable<Integer, Integer>> edges = new Hashtable<>();
private final HashMap<Integer, HashSet<Integer>> emojiId2Message = new HashMap<>();
private final HashSet<Integer> emojiIds = new HashSet<>();
private final Hashtable<Integer, Integer> emojiIdHeat = new Hashtable<>();
可以看出，在这样的设计下，查询的复杂度为O(1)。
其中为了简化查询边的复杂度，edges跟blocktable一样，都是一个二重hashtable，每个id都可以从中取出一个hashtable，只需遍历它即可得到所有与该id相连的所有id。
由于数据结构众多，维护工作也随之变得复杂，这里的一个技巧是所有维护工作在相应的增加人员或增加边的函数中进行。同时我也体会到，尽管我通过数据结构大大优化了程序的运行速度，但是代码的可维护性和复杂度也成倍提高，对我的编程能力和测试能力提出了挑战。
标签：访问 产生 ons require ase heat get 推理 length
原文地址：https://www.cnblogs.com/maxorao/p/14826732.html
