面向对象程序设计第三单元总结
本单元的作业背景是在给出的接口功能要求下根据JML规格进行程序设计，最终按照要求实现对于社交网络的模拟，主要进行学习的点在于接触到JML这个全新的用注释的方式来表达规格的方式，同时对于代码规格以及代码实现的关系也有相应的学习。除此之外，本单元作业的另外一个考点是对于算法的优化，本单元作业中查询类功能要求较高，且耗时较多，因此需要尝试进行性能上的优化，例如在第三次作业中可以采用对最短路径djistra算法的堆优化，以及判断连通性方面用并查集的思想进行优化，在此不再赘述，在文中进行说明。
JML相关介绍
语言理论基础
JML为说明性的描述行为引入了许多构造，这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范。这些构造使得JML的功能在理论上十分强大。
JML始终位于代码的注释内部，不会对正常的编译产生任何影响，当我们需要利用JML对代码正确性等等进行检查时就需要引入外部工具链，目前可以使用的就是OpenJML的相关工具。
通过本单元作业，我对于JML的理解和使用方式有了一些自己的理解，JML往往通过类似形式逻辑的方式来准确的告诉我们代码实现需要的规格，但是JML并不是强行给我们规定一个必须实现的方式，对于每一个方法，我们都可以自行设计相应的算法，只需要保证和JML的规格以及最后的结果一致。如果我们直接按照JML，将注释“翻译”成为代码，那么虽然正确性上能得到很好的保障，但是我们的代码性能可能会非常差，因为JML中为了使得自己的描述更加清晰直接，在ensures的后置条件中，往往直接使用forall循环的方式进行说明，这样一来，我们的代码复杂度将非常高。简单来说，JML是帮助我们实现功能，并形成约束的，而不是我们写代码的行为指导。
JML工具链的配置
在部署JML相关的工具链时，我遇到了比较多的困难，因为OpenJML系列工具不能直接通过下载安装的方式拿来使用，需要对本地的JDK以及工具链的版本进行适配，在阅读了讨论区以及其他博客中大佬们的介绍，终于拼凑出了可以使用的JML工具。但是不知道因为什么原因，在IDEA中配置OpenJML一直失败，因此最终选择用命令行进行尝试，并最后使得OpenJML可以运行。
在使用命令行时，针对我的机器情况，只能通过-esc参数来进行静态检查，不能通过-exec参数来指定某一个SMT Solver来进行检查，至于其他一些同学提到的必须使用某种Solver才能和windows10适配的情况，我并没有发现。通过下图的输出可以发现，这一类静态检查可能对于逻辑的检查还有一定不足，对于一些等值的判断，不能够充分体现写代码的人设计时的思想，可能会对本身安全的地方出现warning提示。
但是由于对openjml还不够熟悉，我没能发挥出它的最大功效，又对Person类进行了删减，本来我是希望对Group或者Network这种比较复杂的类进行测试的，但其中类的互相调用等产生对package的要求，本人不会配置，最后只能采用Person类进行简单的测试。
JML系列工具链的基本使用是这样的。首先需要通过JML编译器如OpenJML等，编译JML语言的代码，这一步实际上就初步检测了JML本身的语法正确性。之后，可以在编译时加入-check的参数对生成的类文件进行JML规范检查。而本次博客作业中要求部署的SMT Solver则对代码等价性进行验证，另一个工具JML UnitNG则是用来生成Java类文件测试的框架，用于代码的自动化测试。
在使用JML UnitNG的时候，输入指令后出现过各种问题，比如自动生成的测试文件无法找到甚至生成的文件出现异常等。
最后实现了对于Person类的简单测试，但是似乎因为缺乏对工具链的充分了解，并不能改变测试工具使用的策略，导致测试的效率会很低，输入的参数不能根据具体方法的不同而灵活变化，对于实际工作中的帮助比较小，今后需要继续学习相关知识，让JML工具链更好的发挥它们的作用。
架构分析
总的来说，本单元的代码框架相较于前两个单元是更加简单清晰的，本身作为一个互动式的系统，需要完成的任务逻辑简单而直白，并且官方包中的runner类已经帮我们处理好了I/O相关事项，我们只需要根据JML规格进行具体方法的设计即可，下面主要根据类图列出方法调用关系和列举具体的方法种类。
需要检讨的是，我对于JML的学习还不够深入，自始至终都有一些误解，以至于一直都将Person、Network和Group三个类贯彻到底，并没有再做拆分，因此显得结构过于简单并且内部方法太过冗杂。这一点值得注意。
第九次作业
本次作业结构十分简单，仅要求实现一些社交网络的基本查询功能，在这些查询功能中不需要进行复杂的计算等，而添加个人、修改信息。增添关系等对模拟系统的操作只需按照JML来写就可以实现稳定的性能，不再赘述。
第十次作业
本次作业中引入了一个新的接口————Group，简单来说就是在Network内部实现细化，group的添加对我们提出了新的要求，主要在于group的建构和group内部变量的查询等，但是本次作业中查询工作开始出现了计算量陡增的情况，因此不得不进行优化，来面对强测和互测阶段较大的数据集，但是本次作业中不需要运用什么算法，减小计算量的方法很简单，只需要对group内部变量进行动态维护即可，这样，虽然每增加一个人都需要进行一次运算，但是时间复杂度仍然大大降低了。值得注意的是，由于使用了动态维护的方法，那么我们必须考虑到之前已经实现的方法中会不会对group的状态产生影响，凡是产生影响的地方，都要进行维护，这一点，课程讨论区中也有同学进行了详细的说明。
第十一次作业
本次作业对于算法的要求比较高，主要是在Network中增添了许多新的需要查询的变量和特征等，涉及到图论的许多相关知识，并且需要同学们对图论的基本算法做出优化。在最开始设计算法时，我对StrongLinked方法做出了错误的判断，想采用两次bfs方法来进行暴力计算，但是后来发现这种方法不仅时间复杂度高，并且正确性方面也存在隐匿的问题，因为第一遍bfs过程如果对点做了标记，那么就会限制第二遍bfs的正确性，如果不做标记，最后对整个路径去重，则需要极高的时间复杂度，根本不能通过测试，最后，在同学的指点下，我重新学习了图论的相关知识，运用了门杰定理，并做了特判，保障了正确性，并且在性能上尚可接受。
Bug分析
第一次作业操作极为简单，因此无论是在写代码的时候还是在互测阶段，都没有发现自己的问题和其他同学的问题。
第二次作业其实在逻辑上也并不复杂，只不过最开始写代码阶段对JML的一些理解出现了偏差，在阅读Group类中queryValue和queryRelation的规格时，出现了理解上的错误，这里是通过对拍和同学交流发现的，另外在计算年龄的方差时出现了问题，我直接使用了方差的化简公式，但是忽略了精度的影响，导致结果不正确，这里有两种解决方法，一是对公式进行改进优化，二是选择暴力计算方法，本人比较懒，选择了第二种。在这次作业的书写阶段暴露出一个大问题，就是我对Java的对象理解仍然不够充分，虽然已经写了一个学期的OO作业，但是这里还是出了问题，我在修改某个Group的内部状态时，新建了一个新的引用，之后对新的引用做了修改，同时没有映射回去，现在想想，当时脑子里真是一团浆糊。在互测阶段，主要检测出了一部分同学没有采用动态维护方法，导致时间复杂度巨高，超时。同时有一些同学没注意Group的size限制，添加人数超过了1111.
第三次作业，在代码书写阶段没有发现什么问题，但是强测确实WA了好几个点，说到底还是算法设计的不够好，出现了超时，这里需要继续做一些类似djistra算法的堆优化以及并查集优化等等。
感悟
本单元代码量小，但是相应的，有一定思考难度，主要体现在算法的设计上，能够给同学们带来挑战的乐趣，由于助教大大把JML写的非常详细，大多数同学都能通过中测，保障基本分数，同时强测阶段有数据强度，保证了区分度，我认为相较于前两单元，本单元的作业梯度设计是非常合理的。
本单元的学习过程中，我对于JML的学习还不是很充分，但是对于契约式的设计有了一定的理解，同时也意识到规格不是限制我们行为的紧箍咒，也不是指导我们实现功能的红宝书，而是我们实现代码的准则和基本依据，我们要正确认识代码规格的作用。同时，要做到对整体架构有宏观理解。