[BUAA-OO] 第三单元：JML规格化设计

[toc]

架构设计

梳理本单元的架构设计，分析自己的图模型构建和维护策略

​ 图模型的构建只需要严格按照JML规格进行加人（加节点），加关系（加边）即可。图模型的维护主要是指维护整个图的一些属性进而提高查询效率。下面将按照三次作业的迭代顺序进行叙述对图模型的维护策略。

第一次作业

​ 第一次作业相对来说比较简单，我们只需按照官方包的接口和JML规格进行Network，Person，Tag三个类的设计，实现一个简单的社交网络的模拟和查询。

​ 在这次作业中，我们需要对Network动态维护tripleSum来达到系统的性能要求。出于提高代码可读性，我实现了一个Graph类来维护Network中的社交网络图，将对图的操作分离到Graph类实现。

public class Graph {
    private int tripleSum;	// 三角关系数量
    private final HashMap<PersonInterface, HashSet<PersonInterface>> connections;	// 用于构建图

    public Graph() {
        this.tripleSum = 0;
        this.connections = new HashMap<>();
    }

    public void addNode(PersonInterface person) {
        connections.put(person, new HashSet<>());
    }

    public void addEdge(PersonInterface p1, PersonInterface p2) {
        ...
        for (PersonInterface pi : friends1) {
            if (friends2.contains(pi)) {
                tripleSum++;	// 动态维护三角关系数量
            }
        }
        connections.get(p1).add(p2);
        connections.get(p2).add(p1);
    }

    public void removeEdge(PersonInterface p1, PersonInterface p2) {
        ...
        for (PersonInterface pi : friends1) {
            if (friends2.contains(pi)) {
                tripleSum--;	// 动态维护三角关系数量
            }
        }
        connections.get(p1).remove(p2);
        connections.get(p2).remove(p1);
    }

    public int getTripleSum() {
        ...
    }
}

​ 同时，对于第一次作业中的query_tag_age_var，即计算tag中person的age的方差，我们应该避免使用遍历来实现，因为遍历会带来较大的时间开销。解决的方法是动态维护ageSum（年龄和）和ageSumSquare（年龄方和），我们可以以$O(1)$的复杂度实现该查询。

public class Tag implements TagInterface {
    ...
    private long ageSum;
    private long ageSumSquare;
    ...

    @Override
    public void addPerson(PersonInterface person) {
        	...    
        	int age = person.getAge();
            this.ageSum += age;
            this.ageSumSquare += (long)age * age;
        	...
    }

    @Override
    public int getAgeVar() {
        int n = personsMap.size();
        if (n == 0) {
            return 0;
        }
        long mean = getAgeMean();
        long varianceNumerator = this.ageSumSquare - 2 * this.ageSum * mean + (long)n * mean * mean;
        return (int) (varianceNumerator / n);
    }

    @Override
    public void delPerson(PersonInterface person) {
        ...
        int age = person.getAge();
        ageSum -= age;
        ageSumSquare -= (long)age * age;
        ...
    }
}

​ 在这里，我们使用了方差展开公式

$$var = \frac{1}{n} * \sum_i^n (x_i-x_{bar})^2 = \frac{1}{n}(\sum_i^nx_i^2 -2*x_{bar}\sum_i^nx_i + n * x_{bar}^2)$$

​ 需要注意的是，根据JML中对求平均数时除法向下取整的描述，这里不能化成$\sum_i^nx_i^2 - n * x_{bar}^2$的形式，否则会有精度错误。

第二次作业

​ 第二次作业中需要维护的指令是query_tag_value_sum，即某个tag中所有人之间相互关系的关系和。朴素的两层循环的复杂度是$o(n^2)$，显然不可取，因此我们考虑在每个tag中动态tagValueSum这个属性，在每次add_to_tag，delete_from_tag，add_relation，modify_relation时都动态维护tagVlaueSum（其中add_relation特别容易忽视）。这个操作会有很多容易错的地方，下面具体叙述。

public class Tag implements TagInterface {
    ...
    private int tagValueSum;
    
    @Override
    public void addPerson(PersonInterface person) {
        if (person != null && !hasPerson(person)) {
        ...
        Collection<PersonInterface> personSet = personsMap.values();
        for (PersonInterface p : personSet) {
            if (person != null && person.isLinked(p)) {
                this.tagValueSum += 2 * person.queryValue(p);
            }
        }
    }

    @Override
    public int getValueSum() {
        ...
    }

    public void addTagValueSum(int addValue) {
        ...
    }

    @Override
    public void delPerson(PersonInterface person) {
        if (person != null && hasPerson(person)) {
            ...
            Collection<PersonInterface> personSet = personsMap.values();
            for (PersonInterface p : personSet) {
                if (person.isLinked(p)) {
                    this.tagValueSum -= 2 * person.queryValue(p);
                }
            }
        }
    }
}

​ 我们在tag类中实现一些对tagValueSum基本的查询和增减操作，同时在tag中增删人时动态维护tagValueSum，这就解决了由人员变化带来的改变。另一方面，我们还要考虑人员关系变化带来的改变，以modifyRelation为例：

// Network.java
public void modifyRelation(int id1, int id2, int value) {
   	...
    int oldVal = mp1.queryValue(mp2);
    int newVal = oldVal + value;
    for (Tag tag: globalTags) {
    if (tag.hasPerson(mp1) && tag.hasPerson(mp2)) {
            if (newVal > 0) {
                tag.addTagValueSum(2 * (newVal - oldVal));
            } else {
                tag.subTagValueSum(2 * oldVal);
            }
        }
    }
    ...
}

​ 在这里，我们遍历Network中的所有tag，如果某个tag中同时包含这两个人，那么关系值的修改就会导致该tag的tagValueSum变化。add_relation中同理。

​ 另一方面，第二次作业新增了query_couple_sum指令，即寻找互为最好关系的人的对数。为了达到较为理想的性能，我们需要做一个维护：

• 对于每个person，维护他的bestFriend，即与他关系值最大的person。

  这一点的实现较为容易，只需要在每次新增关系和改变关系的时候判断是否需要修改当前的bestFriend。

第三次作业

​ 第三次作业只需要为每个person维护一个“收信箱”即可，考虑到每次接收信息都是放在队首，查询时输出前五项，且接收到的信息不会被删除。我们可以用LinkedList链表较为简单的实现此功能。

public class Person implements PersonInterface {
	...
	private final LinkedList<MessageInterface> messages;
}

@Override
public List<MessageInterface> getReceivedMessages() {
    int size = this.messages.size();
    int limit = Math.min(size, 5);
    return new ArrayList<>(this.messages.subList(0, limit));
}
   
@Override
public void addReceivedMessage(MessageInterface message) {
    if (message != null) {
        this.messages.addFirst(message);
    }
}

性能

分析作业中出现的性能问题及其修复情况，谈谈自己对规格与实现分离的理解

优化分析

​ 一些常见的性能问题和解决方案已经在上文列出了，他们均能在实践中取得较为理想的效果。

​ 这里再讨论一处较为隐蔽，较为难以处理的性能问题。请看如下数据：

ln 300
...			// 使用ln构造一张300个人的完全图 person编号从0到299
ap 300 name 18 
...          // 重复该句1417次，使得社交网络中共有1717个人，person编号从0到1716
ap 1716 name 18
coa 0 1 account
foa 1 1
...			// 重复该句1716次，让全部1717个人都关注这个公众号
foa 1716 1
ca 1 1 0 article
...			// 重复该句3433次，使得这个公众号中一共有3433篇文章
ca 1 1 3432 article
da 0 1 0
...			// 重复该句3433次，使得公众号中的3433篇文章全部被删除
da 0 1 3432

​ 这组数据针对的是delete_article指令。

​ 在删除文章时，我们首先要遍历所有person，然后再在person的receivedArticles中删除特定文章。我们常用的储存person收到的文章的数据结构是ArrayList或者LinkedList，这两种数据结构，他们的删除复杂度都是$O(n)$。

​ 这样，单次da的操作次数就是$n*m$，其中$n$是人数，$m$是文章数。

​ 经过估算我们得到上面那样的一组数据，它在10001行的指令里进行了$1,717 *(3433 + 3432 + … + 1) = 10,120,789,537$，超过100亿次操作。

​ 这样的结果显然不能令我们满意。本人使用的是ArrayList，本地测试使用了近50秒才跑完…（考虑到ArrayList的连续存储在这种情况下会优于LinkedList的随机存储，后者的表现可能更劣）

​ 解决的方法是使用双向链表，这种数据结构的增删复杂度可以做到$O(1)$。具体来说，我们使用双向链表来存每个person的article，每篇文章是链表的一个节点。同时，为了快速找到待删除的文章，我们维护一个articleId到节点指针的HashMap。这样就能高效地增删了。

public class Person implements PersonInterface {
	private static class ArticleNode {
        private final int articleId;
        private ArticleNode prev;
        private ArticleNode next;

        ArticleNode(int articleId) {
            this.articleId = articleId;
        }
    }
    ...
    private final HashMap<Integer, HashSet<ArticleNode>> receivedArticleNodeMap;
    ...
    
        
    @Override
    public List<Integer> queryReceivedArticles() {
        List<Integer> list = new ArrayList<>();
        ArticleNode current = this.headReceivedArticle
        ...		// 利用headReceivedArticle输出前五篇文章
        return list;
    }
    
    public void addReceivedArticle(int articleId) {
        ArticleNode newNode = new ArticleNode(articleId);
        if (this.headReceivedArticle == null) {
            ... 	// 添加该节点为首节点
        } else {
            ...  	// 插入节点到中间
        }
        if (this.receivedArticleNodeMap.containsKey(articleId)) {
            // 如果已经有过该文章（本次作业允许重复接收文章）
            HashSet<ArticleNode> set = this.receivedArticleNodeMap.get(articleId);
            set.add(newNode);
            this.receivedArticleNodeMap.put(articleId, set);
        } else {
            ...
        }
    }

    public void removeReceivedArticle(int articleId) {
        HashSet<ArticleNode> removeSet = this.receivedArticleNodeMap.get(articleId);
        if (removeSet == null) { // 一定要有这一步 否则下面遍历会出问题
            return;
        }
        for (ArticleNode nodeToRemove : removeSet) {
            ... 	// 删除该节点
        }
        this.receivedArticleNodeMap.remove(articleId);
    }
}

规格与实现分离

​ 在JML规格化设计中，规格与实现分离是一个核心原则，旨在通过形式化的规格描述与具体的代码实现之间的解耦来提升工程的可维护性和可靠性。

​ 具体地说，规格与实现分离将工程分成了两部分。其中规格关注“做什么”而并不关注具体“怎么做”。规格只给出前置条件，后置条件，不变式等，不涉及也不要求具体实现的算法。而实现则专注于“怎么做”，即高效地实现JML所要求的功能。实现方式上，开发者往往不受限制。

​ 规格与实现分离体现了契约式编程的魅力所在，它使得编程者可以专注于自己的任务，同时也支持团队分工协作。最重要的是，清晰的规格使得进行形式化验证和测试更加容易，增加了工程的可靠性。

测试过程

分析本单元的测试过程

对单元测试、功能测试、集成测试、压力测试、回归测试的理解

数据构造有何策略

测试过程

​ 在本单元的测试中，本人采用了单元测试，自动化测试与构造数据测试相结合的方式。单元测试通过对重难点方法编写Junit测试进行，通过提高覆盖率来验证正确性。自动化测试的目的在于通过大量随机有一定强度的测试核查该次提交的正确性。构造数据测试的目的在于围绕新增函数构造极端的，特殊的样例来测试其最坏的性能表现。

​ 自动测试的数据生成逻辑如下：

单元测试

​ 单元测试用于验证代码中最小可测试单元（如函数、方法）的正确性。在本单元中，我们可以使用Junit编写单元测试数据，并通过行覆盖率，分支覆盖率等指标评估测试的效果，这点将在下文具体陈述。

功能测试

​ 功能测试用于验证系统功能是否符合用户需求，也就是所说的黑盒测试。测试者提供输入，并不关心程序运行过程而只检查程序运行结果。在本单元中，我们在本地编写的测评机就是黑盒测试。进行大量的有一定强度的黑盒测试能够提高我们对程序正确性的信心。

集成测试

​ 集成测试用于验证模块、服务或系统之间的交互是否正确。

压力测试

​ 压力测试用于评估系统在极端负载下的性能和稳定性。在本单元作业中，本人通过增加指令数量（20000行输入），构造极端数据（针对程序中复杂度最高的方法反复询问）等方法进行了充分的压力测试。

回归测试

​ 回归测试是确保代码修改（如修复 Bug、新增功能）后，原有功能未被破坏的测试。这在迭代开发中特别常见。例如我们完成第三次作业后，还应该用第一次，第二次作业的测评机在本地进行反复测试，验证新增功能是否有破坏原有功能。

构造数据策略

​ 以上文针对delete_article方法构造的测试为例，构造数据的策略就是找到自己代码实现中复杂度最高的方法，分析其复杂度高的原因，并针对此原因在数据约束范围构造尽可能复杂的数据进行性能攻击。以本单元作业为例，复杂度超过$O(n)$的方法都有可能成为性能攻击的对象。

大模型辅助体验

根据使用大模型辅助进行规格化设计与代码实现的体验，总结分析如何引导大模型在不同场景下完成复杂任务

大模型使用体验

​ 大模型在给出规格实现代码的任务上表现总体较好，往往可以在一到两次对话中实现一个功能正确的程序。这与JML规格的清晰描述密切相关。

​ 另一方面，给出JML规格给大模型，其实现方法往往是按照JML的描述进行而不会主动优化。例如query_triple_sum的方法中，JML中为了方便描述，给出三重循环的实现方法。大模型根据此规格给出的回答也是朴素三重循环，这样的实现显然难以令人满意。

​ 因此，我们还需要针对代码中实现复杂度较为高的方法进行手动修改或者给出实现方法，要求大模型按照我们指定的方法/算法完成工作。

​ 最后，如果采用了大模型给出的代码，不可缺少的一步是按照JML规格一行一行地进行人工检查，惟其如此我们才能对代码的可靠性有一定的信心。

如何引导大模型

​ 本人自己总结出的规律是先给出要求让大模型写出一个初版，然后自行核查这个初版。对于其中不令人满意的地方，应该具体地指出使用的算法或者实现框架，要求大模型按照所指定的算法或者框架去完成工作。

​ 在测评机的编写上，我们同样可以使用大模型辅助。直接将整个测评机编写任务交给大模型的收效同样很差。因此，本人采取的做法是手工搭建评测机的处理框架，将部分函数的实现交给大模型，同时用注释的方式清晰地指出在这个地方需要大模型以怎样的方式执行怎样的操作。

Junit单元测试

本单元中同学们实现了Junit测试方法，总结分析如何利用规格信息来更好的设计实现Junit测试，以及Junit测试检验代码实现与规格的一致性的效果

基于规格的数据生成

​ 在基于规格的数据生成中，我们希望构造的数据能够覆盖JML规格中所有的情况。包括所有合法状态和异常状态。一般地，针对一个特定的方法编写单元测试，我们可以设置

• 1-3组合法状态，尝试覆盖全部地合法分支
• 1-3组异常状态，尝试覆盖全部地异常抛出
• 1-3组边界状态，例如空图，空关系图和完全图

​ 同时，我们还应在每次调用被测函数后检查是否满足assignable要求，确保没有做超出JML规格允许范围的修改。

​

学习体会

​ 在本单元的学习中，我深刻地感受到了契约式编程清晰，可靠的魅力。规格与实现的分离既增加了代码的可靠性，可维护性，又解耦了实现的复杂度（明确规定了每个方法做什么，不做什么），使代码逻辑更加清晰。

​ 同时，本单元学习还使得我对使用大模型辅助学习有了更深刻的感悟：对于大模型这种先进的工具我们不应当盲目地排斥。堵不如疏，我们应该像使用计算器那样，把大模型当成一种辅助工具而非完全依靠。具体地来讲，在这单元学习中，我学会了如何使用大模型完成复杂任务，同时也深刻地体会到了大模型在理解复杂文本和优化性能上的不足。

​ 最后，我还在这一单元学习到了很多进行测试的手段。除了传统的大量随机测试（测评机）的方式，我还尝试了单元测试，压力测试等方式。构造性能测试的数据的过程也加深了我对算法实现和数据结构（容器）的认识与理解。