面向对象第三单元总结

Posted 2021-05-29 AsaBaka

作业

(1)面具之下

总结分析自己实现规格所采取的设计策略 & 总结分析容器选择和使用的经验

​ 在面向对象的思想中, 一个对象可以被理解为一组数据以及在数据上的操作. 因此基于JML规范来实现具体对象的过程中, 其首当其冲的考量就是数据的存在方式.

​ 数据何以能。人话说就是容器的选取. JML规格中对数据的描述实质上是一种抽象, 是数据在调用者视角上的存在形式。比如在规格中以数组形式存在，其具体实现可以根据最终需求综合决定——也许为了提高查找效率而选择哈希表，也许为了减缩空间而改换其他数据格式，等等。但无论如何实现， 最终对外暴露的行为总是一致的——总是符合JML格式规范的。

​ 当然了，实现规格的过程总是个系统工程，甭说更大规模的软件项目了，在作业中如此小规模的代码实现，数据的存放总是在拿到规格那一刻起就需要着手考虑，随着设计思路的逐步清晰才能逐渐定型，是一个需要反复权衡的设计对象。

​ 同时，数据的存放总是依赖于具体场景需求，规格对行为的抽象给予了实现上的自由，但是吧，拥有自由不一定就是幸福的。我们需要细细考察各处JML规格对对象的约束——也许几行就会让你头大，也许几十行废话搞得人不知所云。

​ 总之吧，总之，我们需要从散落在各个类、各个方法的JML规格中提炼出对数据的操作方法，然后思考如何实现以最好地满足各处需求，甚至还要权衡利弊，找个折中——所幸这几次作业中少有需要权衡的场景。

​ 比如在三次作业中，为了便于增删改查，无论是Person、Group还是Message都采用Hashmap进行存放，而对Person类中messages的来说， 采用List存放能满足规格约束（毕竟返回值都是List），也不会带来性能上的损失。

​

​ 数据如何存放确定后，数据最基础的操作方式也就随之确定。接下来呢？接下来还不能动手实现，虽然通过规格描述已经可以实现出许许多多的方法（以被/*pure*/修饰的方法为代表）。但总归是有些方法需要进一步设计——比如需要更高效的算法——而这些设计并不总是偏安一隅，有时具体实现中需要别处方法的助力：也许一记标记，也许是数据的更新，也许要另外输出个你好世界，有些设计甚至会和全局架构息息相关（为了点性能=.=）。

​ 比如规格约束中Group的addPerson方法只需要将一个Person存好即可， 但是由于Group对象具有维护ageMean、ageVar两个抽象属性，在addPerson同时维护该属性则能避免getAgeMean()每次查找ageMean时需要轮询所带来的性能损失。

​

​ 这样的实现难免会增加耦合性（说实话耦合这个词有点帅还有点怪，但架构设计者总不会喜欢），总归也是没办法的事，只要对外实现了规格抽象，面具之下你里面是mm还是恐龙，我想都没有什么关系。

(2)梳理自己的作业架构设计，特别是图模型构建与维护策略

第一次作业

​ 第一次作业主要实现了MyPerson和MuNetwork两个类. 前者在第一次作业中主要负责维护其熟人列表, 以及和对应熟人在图结构中边的权值. 采用Hashmap的方式以id为索引分别存放具体的熟人Person和权值value.

​ 容器的选择中也考虑过将熟人列表Hashmap acquaintance和权值列表values合并, 只留下一个以id为键值, value为权值的Hashmap, 但是这样破坏了规格对类型的约束(因为实际上并没有存储规格中要求的Person对象), 并且担心后续可能会添加其他和Person相关的操作, 就没有采用这种更为简化的存储方式.

​ MyNetwork则用HashMap people存放了图结构中的所有Person. 基本操作均围绕people展开, 根据JML规格能很轻松地写出来, 不过这时已经暴露出JML规格的不足之处——虽然精确,但过分啰嗦, 比如对addRelation的JML描述是实际实现的好几倍长, 固然有时可以说规格本身比实现难以书写, 但在这种简单的场景总会把问题复杂化.

​ 图结构的构建就是基于HashMap people, 我将图结构的操作抽象为一个工具类GraphTool, 用全局静态函数的方式进行图结构的访问. 比如分别在GraphTool中实现了isCircle()和queryBlockSum(). 前者采用非递归DFS实现, 后者采用拓扑排序的方式计数连通分量的个数.

​ 另外第一次作业还设计实现了异常计数类ExceptionCounter，用以计数给定id触发异常的次数，有幸用到最后，善哉善哉。

第二次作业

​ 第二次作业新增MyGroup类和MyMessage类. 并新增了部分MyPerson和MyNetwork的方法

​ MyGroup包含了一群人, 除了正常增删查Person之外, 还需要维护这群人的ageMean和ageVar, 因此我选择在addPerson同时维护该属性, 避免了getAgeMean()每次查找ageMean时需要轮询所带来的性能损失。但是对于在Group内传递SocialValue则无能为力, 需要每次添加时对Group内成员轮询一遍, 不过指令条数使得这样处理并不会造成性能瓶颈.

​ MyPerson和MyMessage基本按照规格要求新增方法, 为了匹配规则, 还设置了向Person中新增Message的函数addMessage.

​ MyNetwork中, 除了按规格可以顺利实现的部分. 变化较大的主要分为三部分:

• 新增HashMap messages和HashMap groups用以存放Message和Group
• 由于指令数翻了10倍, 因此为了提高isCircle和queryBlocksum的性能而放弃每次DFS查询的方案, 改用并查集, 以期提升了效率ヽ(￣ω￣(￣ω￣〃)ゝ
• 由于Group的valueSum不仅和其中成员有关, 还和成员间是否邻接有关(isLinked). 因此为了提高查询Group的valueSum的效率, 采用在以下两种情况发生时修改Group所维护的valueSum大小①Group新增或删除成员时②Network中有成员之间新增关系, 这两个成员恰在某Group中

第三次作业

​ 第三次作业中, Message分裂出多种变化. 新增的几个Message类按规格实现即可.

​ MyPerson和MyGroup只需新增加钱/组内送钱的函数即可. MyNetwork中新增

​ 第三次作业真正需要注意的地方有这么几处

• 新增HashMap emojiId2Heat存放 EmojiId到EmojiHeat的映射, 实现对EmojiMessage的管理, 这涉及到好几个方法, 需要注意EmojiMessage的EmojiId和MessageId是不同的.
• sendIndirectMessage()中对于最短路劲的查询. 采用迪杰斯特拉+维护优先队列的方式以提高在图结构中查询的速度. 具体实现同第一次作业类似, 在全局函数GraphTool.minPathLen()中具体实现查询算法.

(3)结合课程内容，整理基于JML规格来设计测试的方法和策略

​ 由于JML自动测试不那么成熟, 在查询部分资料小小尝试了一下后决定放弃利用工具根据JML规格来实现, 因此个人主要使用Junit针对性构造测试数据 + 随机生成对拍来实现.

​ 可行的基于JML规格实现测试的方案可能有:

• 现成工具(不成熟):

  • openJML可以编译检查jml注释的格式, 一定程度上检查类的内容(助教写JML应该没用? 要不括号匹配应该能查出来吧)

  • JMLUnit: JMLUnit可以生成用于在JML注释Java文件上运行JUnit测试的文件的工具, 但是JMLUnit的重点基本放在边界测试和特殊值上, 对于代码逻辑和架构的检查还较为困难.

• 能否通过形式化验证的方法证明Java代码实现和JML规格的等价性?

  SMT(Satisfiability modulo theories)求解器可以验证程序的等价性, 那么我们将JML规格视为一种程序代码, 似乎可以构造一种SMT求解器, 通过形式化的方法来验证规格和代码实现间的等价性.

  当然理想很美好了, 实际还处于Demo演示阶段. 经过完全不深入的调查和猜测, 可能是存在以下难点

  • 求解器的局限性

    理论上来说, 验证两段代码的等价性, 可以分别提取两段代码的语义A, B(比如转换成统一的语义表达式), 然后把问题转化成在形式逻辑层面验证A == B是否永真. 验证永真这一步就是SMT求解器干的事.

    但是有的问题可能求解器也无法确定, 或者需要花费海量资源才能验证。或者时候其实很简单的情况，比如“人生的意义”或者“宇宙的终极奥秘”这种显然答案是42的问题，还需要花老大功夫用SMT求解器形式验证一番，也是有点得不偿失。

    当然实现虽然困难, 这种思路还是有相当的理论价值, 并且避开一些复杂的算法问题(比如最短路或者我晚上吃什么), 纯粹一些if-else式代码的等价性验证貌似还是可以做的.

  • 如何统一提取两段代码的语义?

    SMT求解器验证等价性时, 基于的是两段代码统一的语义. 但常常明知道是同一语言书写的同一功能的两段代码, 抽象出其实际实现的功能也是十分困难, 更别说两种不同的语言(JML规格和Java).

    本来JML就是对Java功能的抽象, 现在为了验证两者等价性, 又要把JML和Java转化成第三种统一的语义表达式, 较给SMT求解器验证, 这不是闲得慌吗?

• Junit单元测试和人肉验证

  由于作业实际代码量较小, 使用Junit测试效果不如人肉查验. 在以后更大型的工程中, 可以针对规格的关键环节采用Junit进行有针对性的设计和自动化测试.

(4)针对本单元容易出现的性能问题，总结分析原因如果自己作业没有出现，分析自己的设计为何可以避免

1. 第一次作业

   • isCircle查询两节点是否可达. 由于数据量较小, DFS或BFS应该都不会存在性能问题
   • queryBlockSum查询图的连通分量个数. 这里需要改写规格, 否则会调用过多isCircle()而导致超时. 采用类似拓扑排序的方式在遍历的同时计数即可

2. 第二次作业

   • 由于数据量翻了10倍, 第一次作业中处理isCircle和queryBlockSum的方式就行不通了. 在第二次作业中赶紧换成并查集, 由于并查集维护简单, 查询时间复杂度非常小, 而且指令中没有删除Person的需求,因此是一个相对完美的解决方案
   • Group的三个抽象属性:valueSum, ageVar, ageMean, 三者都进行了动态维护, 即addRelation()时维护valueSum, 从Group中增删Person时维护这三者的值即可
   • 经过分析, 由于指令个数最多10000条, 因此其余可能出现性能问题的地方并不会暴露出性能问题. 比如queryNameRank(), 疯狂向同一个Group中增删Person等

3. 第三次作业

   数据量不变, 此次唯一可能出现性能问题的就是最短路的查询. 我开始时仅采用迪杰斯特拉算法而没有维护一个到源点距离最短的优先队列, 在互测时被卡掉(在此要感谢助教的大恩大德, 强测中并没有下狠手).

   改过来之后又是一条好汉, 在此按下不表,且听下回分解.

(6)谈谈其他

​ 我的心里只有感激

​ 本单元测试主要放在性能上, 疏忽了单元核心的训练目标, 也就是基于规格实现功能, 而导致强测时有bug被查到.在此我要隆重感谢各位辛勤劳作的助教——尤其是编写测试数据的助教, 幸亏他们秉持着"把鸡蛋放在同一个篮子里"的原则, 我才能勉强苟得几个测试点.

​ 失诸正鹄，反求诸其身

​ 出bug还在强测暴雷, 主要是自己的问题: 阅读规格不细/测试功能性覆盖不全所导致. 一方面这体现了程序规范的重要性, 同时也反映出JML规格本身仍有很大完善空间.

​ 作为程序规格, JML能有效规范开发人员的实现, 通过抽象代码行为的方式统一对象行为; 同时程序规格也不是实现的全部, 在实现规格的过程中, 开发人员仍留有极大的自由, 也需要自行设计, 权衡以至最后实现.

​ 同时在阅读JML的过程中也发现一些可改进的空间: 复杂!=重要. 出于形式化表述的需求, 有些JML语句力求精确, 却变得十分臃肿, 也许只是从队列中删去一个元素, 就需要写上数行规格——这在很多时候是不必要的. 就如同UML一样, 具有强大的建模和表述能力, 统一的图示法更有助于交流, 但是复杂的语法规范很多时候就成了一种繁文缛节, 精确统一表述的要求下, 导致需要在很多不必要的细节上浪费时间.

​ 正如过度定义需求很危险一样，过度定义问题的解决方案也是很危险的。

​ 书写出规范的规格不是最终目的, 表示法只是记录系统行为和架构的工具, 规范有效的需求最终目的是清晰表述, 直指需求以期最终解决问题. JML语言很难突出问题的核心, 从这一点上讲, JML并不适用于大规模开发.

​ 最后, 不论JML完善与否, 第三单元强调的规范开发的思想都值得思考学习, 无论是开发项目还是做其他事, 有计划有方法地设计和思考, 总归会对结果有所帮助.