本文主要是介绍BUAA OO Unit3 —— Java Modeling Language(JML)，对大家解决编程问题具有一定的参考价值，需要的程序猿们随着小编来一起学习吧！

BUAA OO Unit3 —— Java Modeling Language(JML)

by Monument_Valley

0. 写在正文前

本篇博客是对笔者在北航2022年春季《面向对象设计与构造》课程第三单元的三次作业的总结。

本单元的主要任务为：学习JML语言，学会阅读并撰写JML，理解契约式编程，并在助教已给出的JML规格下完成一个基于社交网络下的模拟社交软件。

顺便提一句，在读往年博客的时候，从来没有学长对JML这个东西做个简介，让后辈的萌新们对JML这三个字母感到十分迷惑（百度搜索“JML”，前面的搜索结果基本都是我航历代康皮特学子撰写的博客，正版与盗版杂糅，根本看不懂JML到底是个什么东西）。其实这东西就像是那种“不学就不懂，学了就懒得解释”的东西，在此斗胆给各位后人留一点提示。

先给个Wikipedia的解释：

The Java Modeling Language is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler.

说白了，这就是一种描述你的程序“在所描述的情况下应该做出的反应”（这不就是描述测试规格吗。。。）比方说，你手上有一个由这个所谓JML语言书写的规格，还有一个程序，你现在要对它做黑箱测试。你不知道程序到底写了一些什么，但你可以从JML书写的规格中知道某些程序内的方法在获得某些输入后，其内部状态应该发生什么变化，然后你通过输出来测试这个程序的完备性。当然，你构造测试数据来随机测程序肯定不是形式化验证，但一套由JML这种足够严谨的语言来书写的代码规格确实从某种程度上可以帮助你做一些代码的形式化验证。同时，在保障JML语言的严谨性的时候，你也会从JML语言中推导出你的程序该怎么写。

JML语言的一个示例在下图中/* @ */框住的这几行注释内。它就是注释下方的find_first_occurence()方法的规格。别忘了，JML语言描述了这个方法应该做的事情，把JML语言的内容与方法的代码对照着看一看，你可能就能有点对JML语言的感觉了。

蛤？你问我JML里面具体写了些什么？我只能说：“前面的区域，以后再探索吧。”

1. 测试数据的准备

这次作业本质上是对一个社交网络的相关信息管理。最核心的几条指令不外乎这些：queryGroupValueSum（查询特定的带权边权值之和，其中权边满足两个端点都在一个特定点集内）, queryLeastConnection（查询连通块的最小生成树的带权边权值之和）, queryBlockSum（查询图内连通块数量）, sendIndirectMessage（连通块内任意两点间最短距离）。可以看到，从权边权和，到最小生成树，再到最短路径，这个单元的作业的核心问题大多都集中在如何处理图论问题。

针对图论问题准备数据，有如下几点：

1. 准备一些基本的正确性测试数据。好在在上《离散数学2》的时候，马殿富老师使用python教我们图论，因此积攒了一些正确性有一定保证的图论程序帮助我们验证本单元作业中生成图查询结果的正确性。

2. 准备一些压力测试，即测试程序性能。在这方面又能分出几点：1）指令的重复测试；有些人的程序没有保存中间结果（如queryGroupValueSum中，明明在查询的那一刻，没人再往图中填人填关系，所以图的状态是确定的，但有人每次都以一个近乎O(n^2)复杂度的算法遍历所有关系进行查询），那就会产生许多不必要的计算，导致程序超时。2）极端图的测试。有些算法不够高效，对于极端情况没有较为高效的处理（如sendIndirectMessage，这种最短路径问题最经典的算法就是Dijkstra算法，可对于一个数千人串成一个串儿的图，要是用邻接矩阵来作为中间变量存储图，那就将对于一个点来说查询一次就能解决的问题转化为数千次，这要是再重复数千次。。。是吧hhhh）。

然而，这次我其实没写太多数据，更多的专门数据还是请同学帮忙生成了一些。我这回更多的工作是写评测机帮忙跑评测验证正确性与查看程序性能消耗。

2. Homework 9

2.1 容器与维护

第三单元开篇之作，先介绍一些基本的容器设置。

我们需要维护哪些信息？对于每个Person，除了它最基本的id，name与age，我们还要存储与他相关联的Person，以及对应关联的社交值（也就是图的边的权值）；对于Group，要存储id与group内所有的人；对于Network，要存储社交网络中所有人Person和Group。为了方便查询，我采用了HashMap<Integer, Object>的方式进行存储。若采用传统的列表存储，查询时间虽短，但增删的复杂度是O(n)，而邻接表最好情况下查询、增删的复杂度都是O(1)，效率很高，而这种效率的提升在我们的图中拥有数千人时会非常明显；同时，id作为Object的独立、唯一的标识，适合作为HashMap的key。因此采用HashMap作为主要容器。

2.2 算法设计

本次作业最重要的指令有两个：isCircle()和queryBlockSum()。剩余的就是一般查询，现用现查。

isCircle()：核心在于确认两个人是否在一个连通块内。那基础思路就是用一个队列储存即将要访问的点的序列，用一个HashSet标注哪些点尚未被访问。从起点出发，每次取待访问点序列的第一个点。当访问一个点时，将其标记为已访问，把所有与之连接且尚未访问的点放到序列中，重复相关动作。若两个人在一个连通块中，那么一定会被找到。在找到时返回true，若当队列为空时还未找到，则返回false。本次作业还是现用现查。

queryBlockSum()：与isCircle()基本一致，只是在当队列清空时，从待访问的点中抽出一个放到队列中继续寻找，同时计数器+1，当没有待访问的点时，返回计数结果。

可以看到，这两个算法的复杂度基本在O(n)到O(n^2)中间徘徊，而且每次查询都得现算，效率很低。但考虑到本次作业指令压力与图的复杂度不高，因此还可以接受。

剩下的指令就都是基础的查询了。对于一些取平均值之类的指令，算出来就好。

2.3 架构设计

这回的类图没什么好看的。。。把官方包的接口对应的类实现出来就好。

方法复杂度统计（忽略CogC = 0的方法）：

2.4 评测成绩

强测100，无bug。

3. Homework 10

3.1 容器与维护

这次增加了Message类的对象，跟上次作业同理，我们采用HashMap作为存储方式。

由于这回增加了queryLeastConnection()指令，因此会设计到大量求最小生成树的情景，而这又需要关联块作为支撑。因此，向上一次作业一样现用现查用遍历的方式求关联块有极大概率会导致超时。因此，我们采用并查集存储关联块的点，在需要用的时候直接调用，并在添加节点和关系时对这个关联块的并查集做出维护。

由于涉及到具体的图论算法，需要描述带权边的属性，因此我采用设计WeightedEdge的方式，存储带权边的信息。

3.2 算法设计

这次的核心难点是求最小生成树，为此，我先取出给出的人所在的关联块，为关联块内添加所有的关联带权边，并使用Kruskal算法计算得到最小生成树，并算出最小生成树的权和。然而，由于没有提前存储关联块中的带权边信息，导致在调用Kruskal算法之前，还需要遍历寻找所有有关的边，然后才能计算，因此效率还是偏低。

至于平均值、方差之类的命令，由于我这回在增删人与关系的时候就对这些属性进行维护，使得在查询的时候不用现场计算这些数值，进而提升查询图属性时的性能。

3.3 架构设计

这次除了将自己实现的类单独放在一个src下的新文件夹外，还将UnionFind与WeightEdge单独放在一个工具文件夹内，以供随时调用。

复杂度分析如下：

3.4 评测结果

强测100，无bug。

4. Homework 11

4.1 容器与维护

这次图的结构基本确定了，增加了在并查集中维护关联块边集的操作。其实很简单，在并查集中增加一个HashMap<Integer, HashSet<WeightEdge>>，其中Integer用来记录并查集根节点对应的人的id（即作为关联块的标识符），HashSet<WeightedEdge>用来记录边集。在维护并查集的同时，维护边集。除此以外，容器就没什么问题了。

4.2 算法设计

这次的核心指令是sendIndirectMessage()，本质上是一个求一图内两点间最短距离。这一看就是Dijkstra算法所解决的问题。只需要按照正常的Dijkstra算法进行书写便好。但在测试中，由于测试到了前文提到的极端的图，因此修改Dijkstra算法存储图的邻接矩阵，改为遍历acquaintance进行查询。

4.3 架构设计

与Homework10的架构基本一致。

复杂度分析如下：

4.4 评测结果

强测100，无bug。

5. 性能问题

核心问题：在你查询的时候，图的状态是确定的。图只有在加人/加关系的时候，大结构才会发生变化。

因此，在加人/加关系的时候维护好可能要查询的量可以大大降低程序运行时间。

1. 重复查询简单属性的问题

有些属性，例如group的平均年龄，年龄方差之类的数值，我曾经采用现用现查的策略来写。但当我写到查询两人关系的指令时，由于涉及双重循环，因此现用现查策略便会消耗大量算力去计算一个根本不会变的属性（你查询的时候，图的状态是确定的，你反复计算不就是在干无用功吗）。

因此，我在加入/删除 Person/Relationship对象时，便对这些值做出维护，这样在查询这些值的时候，就是一个简单的O(1)查询了。

2. 关联块的建立

我曾经以为关联块无法提前维护，但后来当我注意到“查询时，图的状态是确定的”这一点时，在加人加关系的时候维护好关联块。

3. Dijkstra算法的性能问题

传统上，Dijkstra算法采用邻接矩阵进行维护。但对于特殊图，无用遍历太多，于是我改成了遍历acquaintance进行查询。但还没完。由于寻找最小值的过程算法复杂度也很高，超时风险很高，因此我又进一步使用PriorityQueue进行维护排序，通过这种堆优化算法，终于将Dijkstra算法实现稳定在O(log(n))附近。

6. 关于其他人的bug

大家写得都很完备，确实没查到什么bug。。。看来大家的水平都是很高的。

7. Network的扩展

需要关注广告、发送广告、为产品定价、购买产品等操作。在此给出几个方法的规格：

发送广告：

	/*@ public nomal_behavior
    @ requires containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) && getMessage(id).getType() == 0 &&
    @          getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
    @          getMessage(id).getPerson1() != getMessage(id).getPerson2();
    @ assignable messages, advertiseHeatList;
    @ assignable getMessage(id).getPerson2().messages;
    @ assignable getMessage(id).getPerson1().socialValue, getMessage(id).getPerson2().socialValue;
    @ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&
    @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != id;
    @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
    @ ensures \old(getMessage(id)).getPerson1().getSocialValue() ==
    @         \old(getMessage(id).getPerson1().getSocialValue()) + \old(getMessage(id)).getSocialValue() &&
    @         \old(getMessage(id)).getPerson2().getSocialValue() ==
    @         \old(getMessage(id).getPerson2().getSocialValue()) + \old(getMessage(id)).getSocialValue();
    @ ensures (\exists int i; 0 <= i && i < advertiseIdList.length && advertiseIdList[i] == ((AdvertiseMessage)\old(getMessage(id))).getAdvertiseId();
    @         advertiseHeatList[i] == \old(advertiseHeatList[i]) + 1);
    @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().size());
    @          \old(getMessage(id)).getPerson2().getMessages().get(i+1) == \old(getMessage(id).getPerson2().getMessages().get(i)));
    @ ensures \old(getMessage(id)).getPerson2().getMessages().get(0).equals(\old(getMessage(id)));
    @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == \old(getMessage(id).getPerson2().getMessages().size()) + 1;
    @ also
    @ public normal_behavior
    @ requires containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) && getMessage(id).getType() == 1 &&
    @           getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1());
    @ assignable people[*].socialValue, messages, advertiseHeatList;
    @ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&
    @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != id;
    @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
    @ ensures (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p); p.getSocialValue() ==
    @         \old(p.getSocialValue()) + \old(getMessage(id)).getSocialValue());
    @ ensures (\forall int i; 0 <= i && i < people.length && !\old(getMessage(id)).getGroup().hasPerson(people[i]);
    @          \old(people[i].getSocialValue()) == people[i].getSocialValue());
    @ ensures (\exists int i; 0 <= i && i < advertiseIdList.length && advertiseIdList[i] == ((AdvertiseMessage)\old(getMessage(id))).getAdvertiseId();
    @         advertiseHeatList[i] == \old(advertiseHeatList[i]) + 1);
    @ also
    @ public exceptional_behavior
    @ signals (MessageIdNotFoundException e) !containsMessage(id);
    @ signals (NotAdvertiseException e) !(getMessage(id) instance of AdvertiseMessage);
    @ signals (RelationNotFoundException e) containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) &&
    @          getMessage(id).getType() == 0 && !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
    @ signals (PersonIdNotFoundException e) containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) &&
    @          getMessage(id).getType() == 0 && !(getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()));
    @*/
    public void sendAdvertiseMessage(int id) throws MessageIdNotFoundException, NotAdvertiseException, RelationNotFoundException, PersonIdNotFoundException;

定价：

  /*@ public nomal_behavior
    @ requires (\exists int i; 0 <= i && i < advertiseIdList.length; advertiseIdList[i] == id);
    @ ensures (\exists int i; 0 <= i && i < advertiseIdList.length; advertiseIdList[i] == id &&
    @          \result == advertiseHeatList[i]);
    @ also
    @ public exceptional_behavior
    @ signals (ProductIdNotFoundException e) !AdvertiseIdList.contains(id);
    @*/
    public /*@ pure @*/ int setPrice(int id) throws ProductIdNotFoundException;

购买：

	/*@ public normal_behavior
    @ requires (\exists int i; 0 <= i && i < advertiseIdList.length; advertiseIdList[i] == id);
    @ assignable money;
    @ ensures (\exists int i; 0 <= i && i < advertiseIdList.length; advertiseIdList[i] == id &&
    @          money == \old(money) - advertiseHeatList[i]);
    @ also
    @ public exceptional_behavior
    @ signals (ProductIdNotFoundException e) !AdvertiseIdList.contains(id);
    @*/
    public void buyProduct(int id) throws ProductIdNotFoundException;

8. 心得体会

这次让我学到了一种准确描述程序需求的语言，感受到建立了使用者需求被准确描述后编程的简易性。相较于过往单元指导书内助教所述的程序需求，这次作业的需求明显清晰很多。有疑问的地方也可以通过进一步仔细阅读JML规格找到答案。同时，JML规格为我提供了测试的依据，让我在测试中找到了一些未曾想到的bug。

但注意到的是，JML规格的描述虽说接近于正常程序，但毕竟它不是程序语言，不能直接通过复制其表述来完成编程。在刚开始接触JML时，我对它在简单与复杂问题上冗长的表述感到不解，可当我在编程中真的遇到困难的时候，反而能从这些规格中读出信息，这就是对我们的编程工作的巨大帮助。

也不知道JML语言有没有相关的语言处理器，可以帮助系统读懂需求。。。

不过语言毕竟是人写的，人写的东西难免就会犯错，那该如何对JML语言进行debug呢？希望有助教能够为我们答疑解惑。

这篇关于BUAA OO Unit3 —— Java Modeling Language(JML)的文章就介绍到这儿，希望我们推荐的文章对大家有所帮助，也希望大家多多支持为之网！