心得技巧

html5 HTML/Xhtml CSS XML/XSLT Dreamweaver教程 Frontpage教程心得技巧

上一篇: vue之组件切换下一篇:# cesium 绘制栅栏

BUAA_OO_2022_U3_JML规格

发布时间：2022-06-08 发布网站：脚本宝典

脚本宝典收集整理的这篇文章主要介绍了BUAA_OO_2022_U3_JML规格，脚本宝典觉得挺不错的，现在分享给大家，也给大家做个参考。

第三单元总结

一、测试数据的准备

通过第三单元的训练项目的学习，我尝试了用JUnIT单元测试框架，但是在几次作业的自测中，主要还是使用随机生成数据的方法测试。随机生成数据主要有三个部分：

对每条指令的触发异常部分在生成数据的最开始就对每条指令的异常处理进行覆盖性测试，主要是测试异常处理的基本功能。部分代码如下：

def coverAllException():
	global groupCnt
	global PErsonCnt
	id1 = random.choice(person_ids)
	personId_In.append(id1)
	personCnt = personCnt + 1
	id2 = random.choice(person_ids)
	while id2 == id1:
		id2 = random.choice(person_ids)
	newname = random.sample(alphabet, 10)
	newname = ''.join(newname)
	cmds.append(f'ap {id1} {newname} {random.randint(1, 200)}n')
	cmds.append(f'ap {id1} {newname} {random.randint(1, 200)}n')  # ap exception

	cmds.append(f'ar {id2} {id1} 1n')  # ar exception1
	cmds.append(f'ar {id1} {id2} 1n')  # ar exception2
	cmds.append(f'ar {id1} {id1} 1n')  # ar exception4

因为只是对异常处理的正确性检验，这一部分生成数据主要用于检验完成架构之初的规格实现的正确性，在后续强测找bug过程中可以注释掉这部分。

随机数据的构造主要分为两大部分：正确指令的构造，异常指令的构造。下面给出构造 ar 指令的方法：

def ar():
global cmds
p = random.random()
idIn1 = random.choice(personId_In)
idIn2 = random.choice(personId_In)
idNotIn1 = random.choice(person_ids)
while idNotIn1 in personId_In:
    idNotIn1 = random.choice(person_ids)
idNotIn2 = random.choice(person_ids)
while idNotIn2 in personId_In:
    idNotIn2 = random.choice(person_ids)

if p < 0.45:
    cmds += f'ar {idIn1} {idIn2} {random.randint(1, 1000)}n'
elif p < 0.55:
    cmds += f'ar {idIn1} {idIn1} {random.randint(1, 1000)}n'
elif p < 0.65:
    cmds += f'ar {idNotIn1} {idIn1} 1n'
elif p < 0.75:
    cmds += f'ar {idIn1} {idNotIn2} 1n'
elif p < 0.85:
    cmds += f'ar {idNotIn1} {idNotIn2} 1n'
else:
    cmds += f'ar {idNotIn2} {idNotIn2} 1n'

在后来的测试中发现，使用if-else结构生成数据（else生成触发异常的指令）异常指令占比仍然较高，达不到强测的效果，考虑到第一部分已经对异常处理做了覆盖性测试，可以将id的生成简化为id = random.randint(0, PERSON + 5) 这一部分是类似于JUnit测试的工作，针对每个方法规格的前置条件生成数据，在对拍过程中检验方法的后置条件等实现的正确性。

针对@R_397_1304@限制的数据构造主要是针对qgvs、qgav等指令进行单独大量的数据构造。比如我在第10次作业中发现有人的qgav方法复杂度超过了O(n^2)，于是我构造了一个包含1111个Person的Group，剩下的指令全部为qgav。这也是本单元hack的基本思路：阅读代码 + 定点爆破。

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

本单元架构设计主要就是根据JML实现了自己的Person、Group、Message等类，除此之外，还建立了一个Egde类，用于记录person之间的关系，体现图中的边结构。

图模型构建和维护策略 2.1 维护策略除去可以依照JML规格直接实现的部分以外，还进行了一下的一些维护：

在Person类中用优先队列维护了person之间的关系（Edge类）
在Group类中维护了valueSum、ageSum和ageSqure三个属性，使指令的时间复杂度为O(1)
在Network类中维护了blockSum属性，在addPerson和addRelation时会被修改，用来记录当前的连通分支数，使qbs指令的时间复杂度为O(1)
对于每一个有id属性的对象的存储，都采用HashMap，方便O(1)查找 2.2 图模型的构建 qci采用了并查集和路径压缩的方法，qbs采用动态维护blockSum属性的方法，qlc的最小生成树使用了堆优化的PRim算法 2.2.1 路径可达采用并查集和路径压缩的方法降低时间复杂度，维护了一个father的HashMap容器

private HashMap<Integer, Integer> father = new HashMap<>();   // <child, father>

public int find(int p) {
    if (father.get(p) != p) {
        father.put(p, find(father.get(p)));
    }
    return father.get(p);
}

public boolean isCircle(int id1, int id2) throws PersonIdNotFoundException {
    if (!contains(id1)) {
        throw new MyPersonIdNotFoundException(id1);
    } else if (contains(id1) && !contains(id2)) {
        throw new MyPersonIdNotFoundException(id2);
    }
    return find(id1) == find(id2);
}

2.2.2 最小生成树采用堆优化的Prim算法

public boolean edgeQualified(int id, Edge edge) throws PersonIdNotFoundException {
    Person person1 = edge.getPerson1();
    Person person2 = edge.getPerson2();
    return isCircle(id, person1.getId()) &amp;& isCircle(id, person2.getId());
}

public int queryLeastConnection(int id) throws PersonIdNotFoundException {
    if (contains(id)) {
        ArrayList<Person> subgroup = new ArrayList<>();
        for (Person p : people.values()) {
            if (isCircle(id, p.getId())) {
                subgroup.add(p);
            }
        }
        if (subgroup.size() == 1) {
            return 0;
        }

        HashMap<Integer, Person> personInMinGroup = new HashMap<>();
        PriorityQueue<Edge> edges = new PriorityQueue<>(Comparator.COMparing(Edge::getValue));
        MyPerson person = (MyPerson) subgroup.get(0);
        edges.addAll(person.getEdges());
        personInMinGroup.put(person.getId(), person);
        int value = 0;
        Edge edge;
        while (personInMinGroup.size() < subgroup.size()) {
            while ((edge = edges.poll()) != null) {
                if (edgeQualified(id, edge) &&
                        !personInMinGroup.containsKey(edge.getPerson2().getId())) {
                    //System.out.println(edge);
                    value += edge.getValue();
                    person = (MyPerson) edge.getPerson2();
                    personInMinGroup.put(person.getId(), person);
                    edges.addAll(person.getEdges());
                    break;
                }
            }
        }
        return value;
    } else {
        throw new MyPersonIdNotFoundException(id);
    }
}

2.2.3 最短路径采用最短路径算法dijkstra，实现代码如下

	HashMap<Integer, Person> vertexList = new HashMap<>();
        HashMap<Person, Integer> sufNodes2Value = new HashMap<>();
        PriorityQueue<Edge> edg = new PriorityQueue<>(Comparator.comparing(Edge::getValue));
        vertexList.put(person1.getId(), person1);
        for (Edge edge : person1.getEdges()) {
            sufNodes2Value.put(edge.getPerson2(), edge.getValue());
            Edge newEdge = new Edge(person1, edge.getPerson2(), edge.getValue());
            edg.add(newEdge);
        }
        MyPerson person = (MyPerson) edg.poll().getPerson2();
        while (!person.equals(person2)) {   // when to quit ?
            if (!vertexList.containsKey(person.getId())) {
                vertexList.put(person.getId(), person);
                int edgeValue = sufNodes2Value.get(person);
                for (Edge newEdge : person.getEdges()) {
                    int value;
                    if (!vertexList.containsKey(newEdge.getPerson2().getId())) {
                        if (!sufNodes2Value.containsKey(newEdge.getPerson2()) ||
                                newEdge.getValue() + edgeValue <
                                        sufNodes2Value.get(newEdge.getPerson2())) {
                            value = newEdge.getValue() + edgeValue;
                            sufNodes2Value.put(newEdge.getPerson2(), value);
                            edg.add(new Edge(person1, newEdge.getPerson2(), value));
                        }
                    }
                }
            }
            person = (MyPerson) edg.poll().getPerson2();
        }

三、分析代码实现出现的性能问题和修复情况

在对拍过程中，自己的代码跑的时间更长，简单分析之后，可能是因为一些方法我的实现是O(n)，并不会造成测试TLE，不过后来还是进行了优化和维护。在优化过程中，也发现了一个会造成bug的点，在实现queryGroupAgeVAR的时候，如果处理的顺序不当，由于int的取整，逻辑上与JML规格有出入。错误的实现：

int ageMean = getAgeMean();
if (people.size() != 0) {
	return (ageSquare - ageMean * ageMean * people.size()) / people.size();
}

正确的实现应该是(ageSquare - 2 * ageMean * ageSum + people.size() * ageMean * ageMean) / people.size();

四、对Network进行扩展，并给出相应的JML规格

假设出现了几种不同的Person

Advertiser：持续向外发送产品广告

Producer：产品生产商，通过Advertiser来销售产品

Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买

所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息

Person：吃瓜群众，不发广告，不买东西，不卖东西

如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径

增加的类：Producer、Advertiser、Customer、Advertise，其中Producer、Advertiser、Customer实现Person接口，Advertise糅合了产品和广告两类性质（这样应该不太好，但是能简化一下实现） Advertise类中应该至少包含生产商Producer和广告商Advertiser，广告投放的群组Group，广告费用，产品售价，以及其他广告相关的信息。 Network类增加public instance model non_null Advertise[] productList、public instance model non_null Advertise[] advertiseList 属性。

产品生产商生产产品 Producer通过Advertiser来销售产品，于是Producer创造一个Advertise代表其销售的一类产品。

/*
    @ public normal_behavior
    @ requires !(exists int i; 0 <= i && i < productList.length; productList[i].equals(product)) &&
    @          (product.getGroup().hasPerson(product.getProducer())) && 
    @          (product.getGroup().hasPerson(product.getAdvertiser()));
    @ assignable productList;
    @ assignable product.getProducer().money, product.getAdvertiser().money;
    @ ensures productList.length == old(productList.length) + 1;
    @ ensures (forall int i; 0 <= i && i < old(productList.length);
    @          (exists int j; 0 <= j && j < productList.length; productList[j].equals(old(productList[i]))));
    @ ensures (exists int i; 0 <= i && i < productList.length; productList[i].equals(product));
    @ ensures product.getProducer().getMoney() == old(product.getProducer().getMoney()) - product.getCommercialFee();
    @ ensures product.getAdvertiser().getMoney() == old(product.getAdvertiser().getMoney()) + product.getCommercialFee();
    @ also
    @ public exceptional_behavior
    @ signals (EqualAdvertiseidException e) (exists int i; 0 <= i && i < productList.length;
    @                                     productList[i].equals(product));
    @ signals (ProducerIdNotFoundException e) !(exists int i; 0 <= i && i < productList.length; productList[i].equals(product)) &&
    @                                      !(product.getGroup().hasPerson(product.getProducer()));
    @ signals (AdvertiserIdNotFoundException e) !(exists int i; 0 <= i && i < productList.length; productList[i].equals(product)) &&
    @                                      (product.getGroup().hasPerson(product.getProducer())) && 
    @                                      !(product.getGroup().hasPerson(product.getAdvertiser()));
 */
addProduct(Advertise product) throws EqualAdvertiseIdException, ProducerIdNotFoundException, AdvertiserIdNotFoundException;

Advertiser发送产品广告

/*
    @ public normal_behavior
    @ requires (exists int i; 0 <= i && i < productList.length; productList[i].getId() == id) && 
    @             !(exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == id)
    @ assignable advertiseList, productList;
    @ ensures !(exists int i; 0 <= i && i < productList.length; productList[i].getId() == id) && 
    @         productList.length == old(productList.length) - 1 &&
    @         (forall int i; 0 <= i && i < old(productList.length) && old(productList[i].getId()) != id;
    @             (exists int j; 0 <= j && j < productList.length; productList[j].equals(old(productList[i]))));
    @ ensures (exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == id) && 
    @         advertiseList.length == old(advertiseList.length) + 1 &&
    @         (forall int i; 0 <= i && i < old(advertiseList.length) && old(advertiseList[i].getId()) != id;
    @             (exists int j; 0 <= j && j < advertiseList.length; advertiseList[j].equals(old(advertiseList[i]))));
    @ also
    @ public exceptional_behavior
    @ signals (ProductIdNotFoundException e) !(exists int i; 0 <= i && i < productList.length; productList[i].getId() == id);
    @ signals (EqualAdvertiseIdException e) (exists int i; 0 <= i && i < productList.length; productList[i].getId() == id) && 
    @                                         (exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == id);
*/
sendAdvertise(int id) throws ProductIdNotFoundException, EqualAdvertiseIdException;

消费者购买产品

/*
    @ public normal_behavior
    @ requires (exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == advertiseId) &&
    @                getAdvertise(advertiseId).getGroup.hasPerson(getPerson(personId));
    @ assignable getAdvertise(advertiseId).getProducer().money, getPerson(personId).money; 
    @ ensures getAdvertise(advertiseId).getProducer().getMoney() == old(getAdvertise(advertiseId).getProducer().getMoney()) + getAdvertise(advertiseId).getProductPrice();
    @ ensures getPerson(personId).getMoney() == old(getPerson(personId).getMoney()) - getAdvertise(advertiseId).getProductPrice();
    @ also
    @ public exceptional_behavior
    @ signals (AdvertiseIdNotFoundException e) !(exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == advertiseId);
    @ signals (PersonIdNotFoundException e) (exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == advertiseId) && 
    @                                         !getAdvertise(advertiseId).getGroup.hasPerson(getPerson(personId));
 */
buyProduct(int personId, int advertiseId) throws AdvertiseIdNotFoundException, PersonIdNotFoundException;

有待开发的功能：生产商决定投放广告数量，生产产品的数量，商品销售额及销售路径的查询功能……

五、本单元学习体会

本单元学习了JML的契约式编程，因为不需要自己设计架构，难度比前两单元要友好一些。最主要的收获是能够读懂并实现JML规格，而对于自己写JML规格的能力，这一方面仍然很薄弱，仅在实验和讨论部分进行了少量的训练学习。通过对JML的学习，我体会到JML对前置条件和后置条件的严格定义使得实现和维护代码变得容易，不再会担心产生新的神秘bug令人秃头，除了实现的正确性以外，只需要考虑性能问题。

脚本宝典总结

以上是脚本宝典为你收集整理的BUAA_OO_2022_U3_JML规格全部内容，希望文章能够帮你解决BUAA_OO_2022_U3_JML规格所遇到的问题。

如果觉得脚本宝典网站内容还不错，欢迎将脚本宝典推荐好友。

本图文内容来源于网友网络收集整理提供，作为学习参考使用，版权属于原作者。
如您有任何意见或建议可联系处理。小编QQ：384754419，请注明来意。

标签：bug HashMap java list php python while while 优化优化开发开发查找查找程序员程序员算法算法

上一篇: vue之组件切换下一篇:# cesium 绘制栅栏

猜你在找的心得技巧相关文章

clion结合vcpkg以及GTest的使用 2022-07-07
EGF 2022-06-06
ExtJS 布局-Column布局（Column layout） 2022-06-05
颜色之ARGB与RGB、RGBA的区别与介绍 2022-04-15
rgba中的a是什么意思 CSS之RGBA颜色指南 2022-04-15
rootfs -根文件系统制作 2022-07-07
网页简单布局之结构与表现原则分享 2022-04-15
小项目中怎么防止Vue的闪现画面效果 2022-04-15
隐藏 Web 中的元素方法及优缺点教程详解 2022-04-15
告别硬编码让你的前端表格自动计算的实例代码 2022-04-15

全站导航更多