概述
本单元完成的任务是模拟网络社区(类似于 bilibili 的视频网站), 并且完成了用户关注网络, 视频互动, 信息统计以及信息统计功能.
并且在此途中, 以官方包的 JML 规格为规范指导开发, 学习和理解规格驱动开发.
JML 与规格驱动开发
JML 是一种建模语言, 重点在于契约. 其规定逻辑应当如何, 而不关注如何做到.
JML 通过其语法, 例如前置后置条件 require 和 ensure, 以及异常行为与正常行为的要求, 不变与可改变量等的约束,
使得方法的在不同情况下的效果, 副作用等, 以一个形式化的严谨数学语言表述出来.
而这便给实现和调用提供保证.
实现者可以用任意的结构, 算法等来实现 JML 要求的功能, 只需要保证满足 JML 对输入, 输出, 不变量, 异常等各部分的约束即可.
而调用者面对接口也彻底不需要考虑内部实现, 只需要相信其满足其规格, 因此默认它的效果范围和预期行为.
同时, 对同一段话, 不同人的理解不同; 同样的逻辑, 不同的人叙述方式不同; 同样的现实世界, 不同人的尝试不同.
因此, JML 通过语法严格的形式化语言, 防止 NL 的模糊性和多义性对程序开发的影响.
迫使人在设计接口前规范思考程序的条件, 行为, 以及边界情况; 在编写函数时根据语义唯一的表述写出符合设计的代码.
所以, JML 规格是规范我们开发的一个手段, 通过严格编写, 实现 JML, 可以让我们更全面地考虑问题, 提升了程序的正确性.
但是…
Beware of bugs in the above code;
I have only proved it correct, not tried it.— Donald Knuth(1977)
我认为 JML 有其自身的一些问题.
首先是可读性差, 作为寄生在 Java 注释里的一个语言, 尽管可以通过一些插件提供高亮, 但是其奇怪的语法, 例如到处可见的反斜杠, 不可避免地为阅读造成困难.
而且, 成也萧何败也萧何, JML 好在其数学化的形式表达可以避免模糊性, 但是也坏在其形式化的语句,
让人写每一行逻辑的时候都在学离散数学, 加强了人的认知负担, 或许不但更疲惫, 也容易因此出错.
结果对于人来说, 压力可能反而大于考虑边界, 撰写并阅读文档.
而更进一步, 我们说的正确性保障都建立在 JML 正确的基础上, 而作为写代码会出错的人类, 写一个如此复杂的 JML 必然无法做到不出错,
而届时我们就要在 JML 和 Java 代码上两边 debug 了.
同时, 面临现实世界需求快速的改变, 我们要维护的也除了代码和文档, 要多上一份 JML. 并且在可读性本就一般的 JML 中找到变更的逻辑, 在代码里针对修改, 又是一个挑战.
总之, 我认为 JML 有着很好的愿景, 期待着通过制定和遵守契约, 保证开发的全面性, 程序的正确性以及调用的便捷性.
但是也有其理想化的一面, 在现实开发中使用无法不遇到以上的阻力和困境.
也或许因此现实生活中 JML 没有推广开来, 而大家仍然用着有着这样那样缺点的 NL.
JUnit 测试经验
针对 JML 编写 JUnit 重点在于针对规格全面检测:
异常行为
一般出现在规格最底部, 满足一定条件触发, 需要对此单独编写测试, 创造异常条件并检测 是否抛出异常, 抛出异常是否正确.
正常行为
在正确的前置条件下, 我们要检查输出和约束.
首先是输出的返回值(如果有的话), 是否符合 JML 的要求;
其次, 如果 JML 规定了要改变什么变量或者容器, 那么检查这些改变量是否正确改变;
最后是不变量, 针对 JML 可能规定的不变量, 或者对于 pure 的方法, 我们要保证它没有改变不该改变的状态.
因此对于这部分检测, 我认为可以使用 oracle 的方式.
也就是我们在测试类里, 通过类暴露的接口, 重新按照 JML 逐句翻译实现一个待测方法,
随后创建两个相同对象, 一个调用被检测类的方法, 另一个调用测试类实现的方法.
随后对比两者的输出, 内部的变量内容和状态, 从而确定待测类有无不符合 JML 的实现.
通过这样的方法, 可以很好避免测试接口只提供浅拷贝, 因而对同一对象内部容器内容前后对比, 无法断定是否发生错误改变的问题.
迭代过程
第九次作业
本次作业是根据 JML 要求, 搭建 User, Video 和 Network 的主要框架和作为程序入口的主类, 包括字段和基础的方法.
实现了指令
add_user id(int) age(int) name(String)
upload_video uploaderId(int) videoId(int)
follow_user id1(int) id2(int)
unfollow_user id1(int) id2(int)
watch_video userId(int) videoId(int)
query_received_unwatched_videos userId(int)
query_up_followers_age_ratio upId(int)
query_mutual_following_sum
query_shortest_path id1(int) id2(int)在此次作业, 我只针对 JML 的要求创建方法, 也没有深度考虑更好的数据结构, 只在 receivedVideos 使用了 Deque 作为优化.
其次就是针对查询的全局存储, 例如互关对数.
第十次作业
本次作业为用户提供了 coins 等新字段, 为 video 增加了 type 等字段, 以及在类内和 Network 类的对应方法.
这次迭代内容较多, 新增和修改了指令
add_user_coins userId(int) coins(int)
upload_video uploaderId(int) videoId(int) type(String)
like_video userId(int) videoId(int)
coin_video userId(int) videoId(int) amount(int)
forward_video userId(int) videoId(int) followerId(int)
send_comment userId(int) videoId(int) commentId(int) comment(String)
clean_spam_comments videoId(int) keyword(String)
query_best_contributor upId(int)
query_most_popular_video type(String)
purchase_medal userId(int) videoId(int) amount(int)
queryLongestDecSeq在这次迭代, 我更加注意效率和时间复杂度, 因此针对不同字段的特点选择特定容器, 例如使用 HashSet 存储 User 的 following 字段等.
第十一次作业
本次实现了视频推荐系统, 新增和修改的指令不多.
recommend_video user_id(int)
recommend_Nth_up user_id(int) rank(int)
query_most_influential_up type(String)
query_user_profile user_id(int)
queryGlobalBestContributor在这次迭代, 我也没有进行大规模修改, 仅仅忠于 JML, 通过缓存 interest 列表等手段, 减少方法重复调用, 保证了程序效率.
Bug 与原因
我在第二次迭代出现了 bug.
首先是没有注意到 receivedVideo 会由于新增的转发而多次存储同一个视频, 导致用户观看视频后只删除了其中一个元素.
这当然不符合 JML, 但是由于在上次迭代并没有这种情况, 因此这在当时是符合约束的.
可见对 JML 的实现, 由于实现方法不同, 有可能在后续迭代中不能符合约束.
也因此尽管有 JML 的约束, 我们仍旧应该在迭代后全面测试和检查代码, 防止后续更改破坏过往逻辑.
其次是 cleanSpamComments 方法里的字串匹配, 我当时直接使用了 indexOf 方法, 造成了巨大的性能损耗, 最终 TLE.
这确实是对极端数据考虑不足, 因此我后续修改为 startsWith, 尽管还有巨大提升空间, 但总归是够用了.
关于 AI
我觉得 AI 对于针对 JML 编写程序帮助巨大, 由于 JML 本身对人类较为难以阅读, 但是其形式化的特征和考虑问题的全面性,
使得用于知道 AI 进行程序编写很是有效, 可以使得 AI 有效编写正确代码, 并且很好地考虑边界条件.
但是另外, AI 往往会完全依照 JML 逐句翻译, 有时候会忽略容器选择合理性或者运行效率, 尽管有时候已经提醒过了.
这时候往往就需要人来进行审查和优化.
游戏感悟
在编写 JML 我遇到一个问题, 就是并没有帮助我获取必要信息的辅助接口,
因此我只能通过函数名称传递我要获取的信息, 然后不出所料后续对我创造的接口理解存在偏差, 导致逻辑出现一些细微不同.
我认为多人组队的时候, 需要统一用语, 使得大家对同样表述的理解相同.
并且通过文档标准化任务背景, 设计规范等, 以及设计良好的 API 文档等, 从而针对文档交流和开发.
同时做好条件校验, 异常抛出和处理, 进行防御性编程, 防止其他模块不符合规范.
最后就是进行代码交叉审阅和单元检测, 进一步提升代码的正确性保障.