标签：dijkstra res 状态 成绩 工具链 三次 ddr from ati
根据我的理解，JML是一种严谨的规定，以方便需求方和实现方的沟通。需求方只需要给实现者定好JML规格，实现者就可以照着JML规格的要求写程序了。
JML规格有许多等级，包括Level 0, 1, 2, 3, C, X。我们在课程中学的是JML Level 0。
JML规格可以被分为JML表达式，方法规格，和类型规格。
JML表达式可以分为原子表达式、量化表达式、集合表达式和操作符。
常见的有：
\result：代表返回的参数。
\old(expr)： 代表表达式expr在相应方法执行前的取值。
此外还有\not_assigned(x,y,...), \not_modified(x,y,...), \nonnullelements( container ) 等等。
这些表达式都比较好理解，望文生义，常见的有\forall, \exists, \sum, \product, \max, \min, \num_of 等表达式。
方法规格的核心内容是这几个约束：
在课程中涉及的类型规格有两类：
我的JMLUnitNG一直报这个错，我到现在还没解决这个问题。
UML图
第一次作业我仅仅是机械式地把JML规格翻译成代码，若JML规格写的是数组，我就翻译成linkedlist，初期我没有多想linkedlist和arraylist之间的区别，就选了其中一个，结果为第三次作业的CTLE埋下了祸根。
此外，我在MyPerson类中添加了addAcquaintance(Person, int)方法，作用是在MyPerson对象中添加相识的人以及更新他们的亲密度。我也在MyPerson类中添加了getAcquaintance()方法，作用是在isCircle函数调用dfs算法时，得到MyPerson对象的所有acquaintance 的id。
UML图
第二次作业相比第一次作业增加了Group接口，我并没有对架构进行大的更改，而只是按照JML规格翻译成代码。
我把isCircle函数的算法dfs换成了bfs，因为dfs在数据量大的情况下有可能会爆栈。
由于我容器采用的都是linkedlist，而程序的大多数操作都是在容器的尾端添加元素和随机访问容器中的元素，因此相比使用arraylist容器，我的方法复杂度会很高。
由于我并没有对MyGroup中的方法的复杂度进行优化，结果就是我的强测一片CTLE。
在bug修复中，我使用了变量和容器来当作缓存。具体地说，在MyGroup类中，我创建了变量agesum来存储group中所有person的age的总数，这样每次调用getAgeMean()函数时，就不需要重新计算group中所有person的age的总数。对于getRelationSum(), getValueSum(), getConflictSum()这几个函数我也同样应用了这个思想。
更新这些“缓存”的操作都在调用MyGroup的addPerson()函数里，即每当增加一个人进入MyGroup里，就更新缓存。但是，若把两个原来 !islinked() 的人加入MyGroup后，再在MyNetwork里对这两个人addRelation()，则需注意更新他们在MyGroup里的缓存。
UML图
第三次作业在Network中添加了delFromGroup(int, int), queryMinPath(int, int), queryStrongLinked(int, int), queryBlockSum(), borrowFrom(int, int, int)，queryMoney(int)等函数，在Group中添加了delPerson(Person)函数。
borrowFrom(int, int, int)和queryMoney(int)就是简单地用一个arraylist把每个Person的money存储起来，调用borrowFrom和和queryMoney函数时就对arraylist进行操作。
delFromGroup函数 和 delPerson函数是一组关联的操作，需注意的就是删除Person时需更新MyGroup内的各种缓存。
queryMinPath函数是一个求最短路径的函数，可以应用Dijkstra算法，但是有大佬指出不写堆优化的话可能会超时，所以我写了个对优化Dijkstra最短路径算法。
queryStrongLinked函数本来我毫无头绪，再看了讨论区大佬们的帖子后，知道了这是一个把图里的最大点双联通分量分割出来的问题，可以应用tarjan算法。
queryBlockSum函数是求强连通分量的个数。可以使用并查集，在并查集中，若两个Person拥有相同的root，则他们处在同一个强连通分量中。同理，我们可以使用并查集来对isCircle函数求解，这样就省去了一次dfs/bfs的时间，而只需要在并查集中查找两个Person的root是否相等，时间复杂度可以减少很多，对于isCircle这个频繁使用的函数来说是非常重要的。
此外，在bug修复中，我发现虽然我的算法已经优化得很好了，但是还是会发生CTLE，最后查找到原因是在容器身上，只要把linkedlist换成arraylist就好了，这部分在bug分析中会说到。
写第一次作业时觉得太简单了，因为我原本以为作业是需要我们自己写JML代码，结果发现作业仅需要我们实现课程组提供的JML规格，因此就觉得任务轻松了很多，然后提交后也过了中测，我甚至没有检查我的程序第二遍，也没有对程序进行测试，然后强测就杯具了，由于我的强测成绩太差触发了课程组的保护机制，没让我进入互测间。
之前我把isCircle的规格完全理解错了，竟然单纯去判断person数组的第一个和最后一个元素是否是id1和id2对应的Person。因此，我重写了整个isCircle函数，采用了dfs算法。
isLinked函数的的person.getId() == id 这个判断写错了。
MyPerson 里的queryValue判断函数粗心写错了。
第二次作业我只是机械式地实现了JML规格，但是并没有规划好程序的架构，没有考虑我的实现方式的复杂度，结果强测一片CTLE，这次也是没进入互测间。
在getConflictSum函数里增加了对people.length==0时的处理。之前规格修改了，但我没注意到，所以在这里出bug了。
修改了queryNameRank函数，原来的实现方法复杂度太高，超时了。
addtoGroup函数里若(getGroup(id2)).getPeopleLength() >= 1111，则仅需return，这里之前我写错了，不小心抛出了异常。
优化了getAgeMean, getConflictSum, getValueSum, getRelationSum, addRelation函数，不然会超时。
做第三次作业时，我刻意关注了方法的复杂度，想办法降低方法的复杂度，并且针对较常用且较复杂的函数使用JUnit进行了许多测试。最终成绩相比前两次作业还算满意吧，毕竟进了互测间，而前两次作业没进。
在queryStrongLinked函数里判断是否两个节点是否点双连通时，我原先使用的方法是进行两次bfs。第一次是正常bfs，第二次是把第一次走过的结点掩盖掉，再进行bfs。但是我的实现方式有bug，第一次bfs后可能会掩盖掉第二条路径的结点。所以，在bug修复中我把算法换成了tarjan算法，把图中的最大点双连通图分离出来，然后再判断要搜索的两个结点是否在同一个最大点双联通图中。
isCircle函数使用频繁，但是之前实现方式是bfs，复杂度太高了，所以bug修复阶段对其进行了优化，使用了并查集查找根的方式。
此外，在我原来的实现方式中，许多函数都用了linkedlist来进行数据存储，可是由于我并没有需要在linkedlist中间随机增删元素，而只是在linkedlist的尾端添加元素，以及使用index查找元素，对于linked来说，这样的操作的复杂度是O（n）级别的，而若把linkedlist换成arraylist，操作复杂度是O（1）级别的。因此，我把许多linkedlist容器都换成了arraylist，显著提升了效率，通过了原来在强测中CTLE的数据。
经过了三次作业，我对JML规格已经蛮熟悉了，虽然还有很多细节性的地方没有彻底搞清楚。我觉得像JML规格这样描述程序需求的规格还蛮有趣的。
此外，最印象深刻的就是前两次作业强测都得0分，原因包括粗心和没有做好优化（仅仅是机械式地翻译JML规格）。第三次作业我做了很多优化，强测得了30几分，往好的方面想，也算是进步了一点吧。
我觉得这三次作业中第三次作业最让人难忘。在第三次作业中，为了优化程序的时间复杂度，我们需要利用一些算法和数据结构的知识，使我这个菜鸡进步了很多。自从大二下学完数据结构后，就很少碰到图论相关的数据结构了，而第三次作业就让我有机会把曾经所学的应用上，比如tarjan算法和堆优化dijkstra算法。
标签：dijkstra res 状态 成绩 工具链 三次 ddr from ati
原文地址：https://www.cnblogs.com/samuel234/p/12941445.html
