标签：循环   人物   和我   lock   lan   tle   不能   返回   图论   

前言

你以为你学的是JML，你以为你在学规格，你以为你上的课程叫OO。
哦，这些都没有错。
什么程序不能掺点算法题呢？\-_-/

关于JML

JML是什么

JML（java modeling language）是一种描述代码行为的语言，包括前置条件、副作用等等。JML是一种行为接口规格语言 （Behavior Interface Speci?cation Language，BISL），基于Larch方法构建。
通过使用JML，我们可以忽略一个类、一个方法内部的具体实现，专注于描述方法的预期功能，从而把过程性的思考延迟到方法设计中，扩展了面向对象设计的原则。

总结来说，JML是一种用于规格化程序设计的辅助工具。

JML理论基础

JML是一种行为界面规范语言（BISL）。在这种被称为面向模型的编程风格中，我们需要指定方法或抽象数据类型的接口及其行为。

• 方法 或 类 的接口是从程序的其他部分使用它所需的信息。对于JML，这是调用方法或使用属性或类所需的Java语法和类型信息。

  • 方法接口 包括诸如方法的名称、修饰符、参数数量、返回类型、可能抛出的异常等等；属性接口包括名称和类型及其修饰符；
  • 类接口包 括名称、修饰符、包、超类，以及它声明和继承的属性和方法的接口。JML使用Java的语法指定所有这些接口信息。

• 方法 或 类 的行为描述了一组能够执行的状态转换：定义调用方法的一组状态，允许方法可以赋值的一组属性，以及调用状态和返回状态之间的关系。

  • 方法的状态由逻辑断言描述，称为方法的前置条件。这些状态与正常返回可能导致的状态之间允许的关系由另一个称为方法正常后置条件的逻辑断言描述。类似地，这些前置状态与抛出异常可能导致的状态之间的关系由方法的异常后置条件描述。

JML工具链

工具链有……

翻阅JML的网站，会发现JML的工具有很多，洋洋洒洒至少也是10余种。可是仔细观察，其中大多数是对于老版本Java的支持。其实我们现在可能能用上的，就是OpenJML和JMLunitNG。

OpenJML

读取JML书写的方法逻辑，运用SMT Solver对方法进行验证。

JMLunitNG

针对书写的JML规格，生成看似很强的数据用于测试。

JML的使用

其实……

一句话总结：遇到传奇error。
听说是Java版本问题。经过了将近1天的努力，我最终决定，为了不乱改环境（毕竟还有一个单元作业），选择了放弃。

当然……

当然我还是通过各种方式去了解了一下这些工具的使用效果的。

• OpenJML来说，根据往届学长们的博客，这个工具并不支持\forall、\exist等部分语句。显然少了循环体，根本无法完成对本单元所要用到的方法的规格化声明。
• JMLunitNG则是会倾向于设计一些极端数据。这些极端数据是对于计算机，或者说是语言本身设计的，比如去检查int变量是否会越界之类的问题。
  很显然，工具本身肯定无法知晓我们到底要干什么，因此也无法知晓我们程序最危险的地方在哪里。当然，通过这类工具增大测试的覆盖面积还是合适的。

体会

各种方面来说，JML都是不成熟的。当然这也反应着其不易用性。在现在的环境下，JML竟然连新版本Java环境都不支持，其官方手册最后一次更新也是2年前。在如今计算机领域飞速发展的大环境下，JML没有前进便必然被淘汰。
当然，虽然其工具链并不好用，其本身进行一些规定形成一种注释或是设计用的风格还是很值得借鉴的。

作业

设计思路

综述

本单元作业的架构实在是没有什么值得一说的地方，毕竟有什么类、每个类有什么方法都已经被JML定义好了，全年级的同学的程序的架构恐怕都是一样的。要说不同就是实现方式的不同了。
就个人来说，本单元作业自己的设计思路完全是性能驱动，究其原因是课程组发布的说明里面总是跟着这么一句话：

“程序的最大运行cpu时间为2s，虽然保证强测数据有梯度，但是还是请注意时间复杂度的控制。”

其实也没必要说得这么委婉……反正就是卡(kao)性(suan)能(fa)，说明白了没啥不好的。

第一次作业

初来乍到看JML给的要求的时候，直观感觉是：直接照着JML写，问题不大，性能对于这次的测试其实也足够了。但终究还是有一些调整。

• Person
  阅读Person类的规格，怎么看怎么觉得存关系(acquaintance和value)的两个数组很丑陋，因此改变了固定数组的存放，变为HashMap容器，Key存放相关者的ID，Value存放ID对应的value。
  这样省下了一些空间，同时通过哈希结构提升了查找速度。
• NetWork
  其中复杂度最高的方法就是isCircle了。
  开始时选择了广度优先遍历，但之后觉得不稳妥，就学习了并查集的思路，自己构建了一种存储手段：
  1. 存放一个HashMap，Key存放人的ID，Value存放HashSet，内部存储与此人相关联的人的集合；
  2. 每次加入新人时新建一个键值对；
  3. 每次增加人物关系时，把两人对应的HashSet合并，并改变前述HashMap。
     这样做性能相比并查集，存储性能下降，查询性能提升，当然都比广度优先遍历要好。

第二次作业

这次作业的工作重心倾向到了Group这个新加的类之中。组和图的概念在本单元作业里面出现了并行，有点意外。难度主要集中在queryGroupRelationSum、queryGroupValueSum、queryGroupAgeMean、queryGroupAgeVar这四个方法上。整体来说，还是为了性能，我取出来了实现并查集的一部分思路——进入更新。每有一个人加入组中，对保存的属性进行更新。

• queryGroupRelationSum、queryGroupValueSum
  这两个方法十分相似，无非一个每次+1，一个每次+value。直接设两个属性，分别存放两个方法需要的返回值。每有一个人加入组中，遍历其与原组员关系并更新两个属性。
• queryGroupAgeMean、queryGroupAgeVar
  一个是年龄的平均值，一个年龄的方差，考虑到精度问题，我“进入更新”存放的是年龄和以及年龄平方和。这样在需求值的时候只需要进行复杂度为1的计算。

第三次作业

来了来了，图论的东西它来了。

• 有关money
  操作跟闹着玩一样，甚至比第一次作业还简。
• delFromGroup
  看起来有些挑战，但第二次作业更新都不出问题，还原也不会出大问题。当然这里用到了计算异或都一些知识：
  $ A xor B xor B = A $
• queryBlockSum
  见第一次作业，本身自己已经存储了一个HashMap，存放人物ID与其所在集合的对应关系，遍历其中集合有几个便可。但遍历操作无疑复杂度还是高，因此延续运用进入更新想法，设置新属性，每次增加人和增加关系时对这一属性进行更新，复杂度降为1.
• queryMinPath
  读懂JML，加上指导书对value的正数限制，能用的算法其实就两种了：Dijkstra算法和SPFA算法。其实还有常用的Floyd算法，但其主要用于遍历全图，对于我们只需要两个点之间的最短路径，不太合适。
  最终选择了Dijkstra，主要是觉得既然限制了为正权图，用这个稳定的比SPFA要好，虽然我内心是相信课程组不会设点去卡SPFA……
  然后还进行了堆优化，其实主要是考虑到Java本身已经带了PriorityQueue容器了，不用白不用。当然我事后觉得幸好优化了……我不应该因为这是OO课就对课程组的善良抱有希望……
• queryStrongLink
  读懂JML，你发现这就是在求两个点是不是双连通。
  本来想着最多求20次，直接双BFS偷懒，结果讨论区dalao直接画了个双BFS会出问题的图出来。就算我相信课程组的善良，也不会相信自己那么幸运地进了互测，而且屋子里没有XX故意卡你。（再加上自己本地测时候双BFS也没写对）所以我转向了tarjan算法。
  道理我都懂……但这个我真的调算法调了很久——主要是对算法本身理解不够透彻。
  因为tarjan算法本身并不是特殊针对双连通求解，而是求解中顺带可以求出双连通，本来我还想着能简化一下，到最后只是对其加入了Java特有的容器HashSet，也算是进行了一些优化。

BUG

第一次作业

主要问题出在isCircle对应的HashMap的更新上，由于并不是完全按照并查集实现，每次更新需要遍历操作。
这个Bug是自己课下写的时候直接通过“脑内模拟”感觉出来的……
强测和互测都没有翻车。

第二次作业

第一次强测挂零。
第一次没进互测。
嘛……什么事情都要经历一下是吧……

• 更新顺序
  因为选择了“进入更新”的策略，就要不断考虑什么时候算进入……
  对于组来说，“进入”不只是当有人加入组内的时候，还有组内的人增加了新的关系的时候。
  开始我把后者忘了。此处感谢讨论区（虽然没有救我狗命）。
• RE
  求组内年龄平均值和方差时候，会除以组内人数。组里没人的时候，忘记了判定，出现了除以0操作……
  强测2/3没了。
• WA
  JML中限制了组内人数不超过1111。1111这个数太皮了……而且没写这种情况下该怎么办……未定义行为我就随心所欲了，然后强测另外1/3也没了。
  其实我还是处理了一下的，写了一行assert(…)，但自己对Java中assert(…)的行为理解不到位，（事实上这句话就和没写一样……）所以该错还是错了。

第三次作业

其实谈不上Bug，因为自己对tarjan算法的理解问题，自己写的queryStrongLink一直无法正确实现目的。充分理解算法之后就没有问题了。
强测和互测没有翻车。

心得体会

规格

规格化设计是必要的。规格可以让多个人写一个程序的时候，进行很好的分块化处理，方便大家进行交流，方便程序各部分的交互，方便对各部分进行分开测试。
当然，对于个人来说，规格就像是书写良好的注释，提醒自己各部分要干什么，提醒自己哪里可能存在bug。
然而，想要写好规格很难，因为自己会有许多先入为主的设想。想要写出充分条件可能还较方便达成，但规格要求的是写充分必要条件。想要书写良好的规格，需要多加练习。

JML

JML是一个用于对于Java进行规格化设计所用的语言。作为一个语言，它本身算是优秀，虽然有时候括号很多看着不方便，但其进行了严格定义，每种语句本身不会有语义偏差——除非写的不好。
但是其工具链可以说处于不可用状态。
当然我们也需要思考其本身需不需要强大的工具链。毕竟再细化下去，JML就已经不是起到辅助作用，而是可以单独作为一种语言了。

“课程组的善良”

这是一点碎碎念了。最后一次官方给的数据来看，同学们的CTLE错误率已经到达了50%。这真的是面向对象课程嘛……最后摆明了考算法……
当然在前言也说了，什么程序设计用不到算法呢？在这里最多也就吐吐苦水爽一爽。
但有一件事情是值得关注的。测评机真的不稳定。
这很正常，任何一块CPU同时运行多道程序，其每个程序自身速度都会降低。
所以集中所有人进行强测的时候，很多人出现了CTLE。
室友A和我本地对拍时候程序运行时间跟我基本一致，强测CTLE一点，该点数据本地自测跑出来的速度跟我还是差不多。Bug修复也是直接交源代码AC。
在这里也是想，万一自己博客荣幸滴被后辈阅读，一定要把程序各处优化到最好，然后听天由命……

OO Unit3 ViewBack

标签：循环   人物   和我   lock   lan   tle   不能   返回   图论   

原文地址：https://www.cnblogs.com/Suxy-99/p/12939472.html