其他分享
首页 > 其他分享> > 北航2022面向对象第三单元:JML规格

北航2022面向对象第三单元:JML规格

作者:互联网

北航2022面向对象第三单元:JML规格

内容概括

1. 测试方法

因为本单元的JML语法是清楚且严格的,对于一些特别简单的方法就没必要做测试了。但是对于核心和复杂的方法,可以翻译成自然语言进行测试,同时对also区分开的分支全面覆盖。特别注意要一句句翻译,不然容易漏看条件。

比如将Person添加到Group中这个方法。

public void addToGroup(int id1, int id2) throws GroupIdNotFoundException,
            PersonIdNotFoundException, EqualPersonIdException;

异常情况就有三种,要注意判断抛出的异常是什么,传入的id是什么。正常情况,要注意一组的人数有上限,如果不认真看容易看漏。

对于复杂的JML,可以翻译成自然语言进行理解。

比如

/*
求一个值最小的subgroup,一共有偶数个人,而且
(\min Person[] subgroup; subgroup.length % 2 == 0 &&
    0-1,2-3,4-5...这些人有联系,而且
    (\forall int i; 0 <= i && i < subgroup.length / 2; subgroup[i * 2].isLinked(subgroup[i * 2 + 1])) &&
    所有和id这个人在一个圈内的人,
    (\forall int i; 0 <= i && i < people.length; isCircle(id, people[i].getId()) <==>
        也在这个subgroup里面,而且
        (\exists int j; 0 <= j && j < subgroup.length; subgroup[j].equals(people[i]))) &&
    所有和id这个人在一个圈内的人,
    (\forall int i; 0 <= i && i < people.length; isCircle(id, people[i].getId()) <==>
        存在一个connection数组
        (\exists Person[] connection;
            connection第一个人是id对应的人,最后一个是圈内的这个人。而且对于connection中的c[j],c[j+1],在subgroup中有s[k],s[k+1]分别对应。
            (\forall int j; 0 <= j && j < connection.length - 1;
                (\exists int k; 0 <= k && k < subgroup.length / 2; subgroup[k * 2].equals(connection[j]) && subgroup[k * 2 + 1].equals(connection[j + 1]))); connection[0].equals(getPerson(id)) && connection[connection.length - 1].equals(people[i])));
    对subgroup求值,把0-1,2-3,4-5...的连接的权值加起来。让这样的值最小。
    (\sum int i; 0 <= i && i < subgroup.length / 2; subgroup[i * 2].queryValue(subgroup[i * 2 + 1])));
*/
public /*@ pure @*/ int queryLeastConnection(int id) throws PersonIdNotFoundException;

通过自然语言稍加分析,可以知道是求id这个人所在圈子的最小生成树。通过构造不同的连接,计算最小生成树的权值之和,就可以测试这个方法了。

2. 架构设计

主要的方法涉及到并查集、最小生成树、单源最短路径

3.性能优化

本单元作业逻辑没有大的问题,出的问题主要是性能优化问题,导致超时。

4. Network拓展

发送广告

可以并入发送信息里面。给特定的人发广告或者群发广告。

/*@
@ requires    containsMessage(id) && getMessage(id).getType() == 0 &&
@            getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
@            getMessage(id).getPerson1() != getMessage(id).getPerson2();
@ .......
@ ensures    (\old(getMessage(id)) instanceof AdMessage) ==>
@            (\old(getMessage(id)).getPerson2().allAds.length = 
@    \old(getMessage(id).getPerson2().allAds.length) + 1) &&
@            (\forall int i; i >= 0 && i < \old(getMessage(id).getPerson2().allAds.length); 
@                (\exists int j; j >= 0 && j < getMessage(id).getPerson2().allAds.length; 
@    getMessage(id).getPerson2().allAds[j] == \old(getMessage(id).getPerson2().allAds[i])) &&
@            (\exists int i; i >= 0 && i < getMessage(id).getPerson2().allAds.length; 
@    getMessage(id).getPerson2().allAds[i].equals(\old(getMessage(id))));
@ .......
@ .......
@ requires    containsMessage(id) && getMessage(id).getType() == 1 &&
@            getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1());
@ .......
@ ensures    (\old(getMessage(id)) instanceof AdMessage) ==>
@            (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p) && 
@                p != \old(getMessage(id)).getPerson1();    
@                (p.allAds.length == \old(p.allAds.length) + 1) && 
@                (\exists int i; i >= 0 && i < p.allAds.length; 
@                    p.allAds[i].equals(\old(getMessage(id)))) && 
@                    (\forall int i; i >= 0 && i < \old(p.allAds.length); 
@                        (\exists int j; j >= 0 && j < p.allAds.length; 
@                        p.allAds[j].equals(\old(p.allAds[i])))));
@ ......
@*/
public void sendMessage(int id) throws
    RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException;

购买产品

发送一条购买商品的信息

/*@
@ requires    containsMessage(id) &&
@            getMessage(id) instanceof PurchaseMessage &&
@            getMessage(id).getType() == 0 &&
@            getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
@              getMessage(id).getPerson1() != getMessage(id).getPerson2() &&
@            getMessage(id).getPersion1() instanceof Advertiser &&
@            getMessage(id).getPersion2() instanceof Producer;
@ assignable messages, goodsTypes, goodsTypesCount;
@ assignable getMessage(id).getPerson1().socialValue;
@ assignable getMessage(id).getPerson2().messages, 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    (\forall int i; i >= 0 && i < \old(goodsTypes.length);
@                (\exists int j; j >= 0 && j < goodsTypes.length; goodsTypes[j]==\old(goodsTypes[i]) && 
@                    (!(goodsTypes[j] instanceof AdType) ==> goodsTypesCount[j] == \old(goodsTypesCount[j]));
@ ensures    goodsTypes.length == goodsTypesCount.length;
@ ensures    !(\exists int i; i >= 0 && i < \old(goodsTypes.length); \old(goodsTypes[i]) != AdType) ==>
                (goodsTypes.length == \old(goodsTypes.length) + 1) &&
@                (\exists int i; i >= 0 && i < goodsTypes.length; 
@                        goodsTypes[i] == AdType && goodsTypesCount[i] == 1);
@ ensures (\exists int i; i >= 0 && i < goodsTypes.length; 
@            (goodsTypes[i] instanceof AdType) ==> goodsTypesCount[i] == \old(goodsTypesCount[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 exceptional_behavior
@ signals (MessageIdNotFoundException e)
@     !(containsMessage(id) &&
@    getMessage(id) instanceof PurchaseMessage &&
@    getMessage(id).getType() == 0 &&
@    getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
@    getMessage(id).getPerson1() != getMessage(id).getPerson2() &&
@    getMessage(id).getPersion1() instanceof Advertiser &&
@    getMessage(id).getPersion2() instanceof Producer);
@*/      
public void buyGoods(int msgId) throws MessageIdNotFoundException;

查询产品销量

输入产品种类,查看该产品销售了多少个

/*@
@ public normal_behavior
@ requires    !(exists int i; i >= 0 && i < goodsTypes.length; goodsTypes[i] == adType);
@ ensure    \result == 0;
@ also
@ public normal_behavior
@ requires    (exists int i; i >= 0 && i < goodsTypes.length; goodsTypes[i] == adType);
@ ensure    (exists int i; i >= 0 && i < goodsTypes.length; goodsTypes[i] == adType && 
@                \result == goodsTypesCount[i]);
@*/
public /*@ pure @*/ int getSales(AdType adType);

5.总结和体会

本单元主要学习了JML的简单用法。我认为JML和接口的内在思想是相通的,都是规定了任务分工。JML是更好地进行分工而约定的一套接口。每个类、每个方法都只需要考虑有限的几种情况,而不用纠结于比如一个String是否为null,是否为"",是否为" \t "等细小而繁杂的问题,再处理业务逻辑。这样的规定极大减少了重复判断的开销,而且方便了内部的灵活实现,使得检查的方法致力于检查,具体实现方法致力于业务逻辑。至于具体实现则不作限制,只要能满足给定的功能就行。这就很类似于面向接口编程。只规定一套输入输出,具体实现不作要求,通过规范和合理分工,使得不同人、不同时间开发的程序也能很快地对接起来。

写JML程序最大的感受就是省心。只要考虑给定范围内的处理,实现方法也不作要求,凡是不满足require的输入一概不管。深刻体会了合理分工可以带来高效。

标签:JML,int,北航,length,getMessage,2022,&&,goodsTypes,id
来源: https://www.cnblogs.com/mtr329/p/16343208.html