标签:失误 请求 输入参数 配置 -- 异或 注意 orm 实例
JML,全称The Java Modeling Language
,是用于对Java程序进行规格化描述的注释性质语言。
笔者在本文总结了常见的JML语法描述。
在注释行或注释块中,以@
开头的行被认作JML注释行。
//行注释
//@ ensures \result == id;
public /*@pure@*/ int getId();
//块注释
/*@ ensures \result == (\sum int i; 0 <= i && i < people.length;
@ (\sum int j; 0 <= j && j < people.length &&
@ people[i].isLinked(people[j]); people[i].queryValue(people[j])));
@*/
public /*@pure@*/ int getValueSum();
在行为描述中所能够使用的变量,与实现相剥离。
/*@ public instance model non_null int id;
@ public instance model non_null Person[] people;
@*/
关键字 | 描述 |
---|---|
instance |
实例成员,只能通过类型的实例化对象引用。 |
static |
静态成员,可以通过类型引用。 |
non_null |
非空成员修饰。 |
表达式 | 描述 |
---|---|
\result |
表示返回非void方法的执行结果。 |
\old(exp) |
表示在方法执行前exp的取值。 |
\not_assigned(x, y, ...) |
表示方法执行过程中,括号中变量是否被赋值,没有赋值返回true,用于后置条件约束。 |
\not_modified(x, y, ...) |
表示方法执行过程中,括号中变量取值未发生变化。 |
\nonnullelements(container) |
表示container集合或容器对象中没有存放null成员。 |
\type(type) |
返回type对应的类型。 |
\typeof(exp) |
返回exp对应的类型。 |
本单元的作业中只使用到了前三种描述。
表达式 | 描述 |
---|---|
\forall |
对应离散数学中全称量词的概念,表示给定范围内的所有元素均满足约束条件。 |
\exists |
对应离散数学中存在量词的概念,表示给定范围内存在元素满足约束条件。 |
\sum |
对给定范围内的表达式求和。 |
\product |
对给定范围内的表达式连乘。 |
\max |
给定范围内表达式的最大值。 |
\min |
给定范围内表达式的最小值。 |
\num_of |
指定变量中满足相应条件的取值个数。 |
较为常用的是前三种描述,下面是第十一次作业中对于求连通块个数的描述。需要注意的是,\sum
只对其后紧跟的表达式i
进行范围遍历求和,而不应当理解为对i
、j
的遍历均求和;需要参与求和的表达式位于描述的最后,需要细致观察括号的匹配,避免误解规格。
/*@ ensures \result ==
@ (\sum int i; 0 <= i && i < people.length &&
@ (\forall int j; 0 <= j && j < i; !isCircle(people[i].getId(), people[j].getId()));
@ 1);
@*/
public /*@pure@*/ int queryBlockSum();
JML规格可以构造局部集合,一般形式为new ST {T x | R(x) && P(x)}
,在本单元作业中并没有出现这种描述。
JML可以正常使用Java定义的操作符,还包括如下几类。
操作符 | 描述 |
---|---|
<: |
子类型或相同类型返回true。 |
<==> <=!=> |
类比离散数学中的等价。 |
==> <== |
类比离散数学中的蕴含。 |
\nothing |
作用域访问空集。 |
\everything |
作用域访问全集。 |
requires
:对方法的输入参数进行限制,是对用户使用该方法的约束。也就是说,用户输入参数不满足规范,方法的执行结果将不可预测。
ensures
:对方法执行后的结果进行限制,是程序员实现方法所必须遵循的约束,保证方法执行结果的正确性。
assignable
:指定方法可以对对象的哪些属性进行赋值,常与\nothing
和 \everything
搭配使用,也可单独指定类中的一个或多个属性。
/*@ public normal_behavior
@ requires contains(id);
@ ensures (\exists int i; 0 <= i && i < people.length; people[i].getId() == id &&
@ \result == people[i]);
@ also
@ public normal_behavior
@ requires !contains(id);
@ ensures \result == null;
@*/
public /*@pure@*/ Person getPerson(int id);
/*@ pure @*/
:表示方法不对对象进行任何改变。
一些博客中定义其不需要提供输入参数,指导书也疑似定义其不需要提供参数。作业中出现了需要输入参数且标注了pure的方法。笔者查阅了讨论区dalao提供的JML英文手册,pure方法应当是没有对输入参数进行约束的(但笔者英语水平有些鸡肋,理解可能有疏漏),参考链接:7.1.1.3 Pure Methods and Constructors。
笔者更倾向于简单地理解作业中的pure表述为assignable \nothing
,这种方法可以直接在其他方法规格中被引用。
public normal_behavior
:描述方法的正常执行行为,需满足其前置条件约束。
public exceptional_behavior
:描述方法的异常执行行为,需满足前置条件约束,与正常行为的前置条件不能存在交集。
signals (Exception e) P
:当进入异常行为且满足条件P,抛出异常e。
在异常部分中也可以使用ensures
来描述方法的执行结果。
also
:存在两种使用的场合。
/*@ public normal_behavior
@ requires contains(id1) && contains(id2) && getPerson(id1).isLinked(getPerson(id2));
@ ensures \result == getPerson(id1).queryValue(getPerson(id2));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@ signals (RelationNotFoundException e) contains(id1) && contains(id2) &&
@ !getPerson(id1).isLinked(getPerson(id2));
@*/
public /*@pure@*/ int queryValue(int id1, int id2) throws
PersonIdNotFoundException, RelationNotFoundException;
JML实现了对代码规格的严格约束,既避免了一般语言进行注释描述的歧义性,又与代码具体实现相分离,提高了代码的可维护性,在工程中有很强的实践意义。
用于检查JML的语法。
笔者未能成功配置环境并且部署,且普遍评价都是该工具功能有限,无法支持复杂JML语法,已经有多年未维护,遂放弃。
用于随机生成测试用例。这个工具只是生成了大量的边界数据与异常数据,覆盖性较差,并不能起到很好的测试效果。
Java语言的单元测试框架,也就是“白盒测试”。
十分成熟的测试工具,且目前已经普及。在对程序基本功能进行测试时有很大的帮助,可以减少程序员的疏忽导致的Bug,但是难以做到复杂逻辑的覆盖性,适合于开发过程中使用。
针对作业进行数据构造,然后与其他dalao完成对拍工作,也就是“黑盒测试”。
这种测试可以模拟强测条件,较为全面地测试程序的鲁棒性,适合开发完成后使用。
对比白盒测试Junit与黑盒测试对拍两种方式:
白盒测试 | 黑盒测试 | |
---|---|---|
使用节点 | 开发过程中 | 开发完成后 |
测试要素 | 功能性 | 鲁棒性 |
检查错误 | 低级代码失误 | 逻辑错误、程序性能 |
测试缺陷 | 单元测试编写与代码的思维一致,可能都对规格理解有误;复杂数据难以手动构造。 | 对拍的程序可能存在相同错误;很多情况下不一定存在可对拍的程序。 |
本单元三次作业基本依据JML规格进行代码编写,对于类的层次化设计并不明显。前两次没有自行设计类和接口,第三次只设计了简单的Edge
类和DijkstraPair
类,因此没有绘制UML类图。
NetWork
方法分析整个关系网呈现一个无向图结构,人作为点,关系作为边,value
作为边的权值。
contains(int id)
:检查图中是否包括编号为id
的点。getPerson(int id)
:获取图中编号为id
的点对应的Person
对象,如果没有,返回null
。addPerson(Person person)
:向图中添加点。addRelation(int id1, int id2, int value)
:向图中两点添加权值为value
的边。queryValue(int id1, int id2)
:返回id1
与id2
的边权值。queryConflict(int id1, int id2)
:返回id1
与id2
的character
异或值。queryAcquaintanceSum(int id)
:返回id
的邻接点数量。compareName(int id1, int id2)
:返回id1
和id2
name
的字典序比较。queryPeopleSum()
:图中点的数量。queryNameRank(int id)
:id
的name
在所有人中的字典序排名。isCircle(int id1, int id2)
:id1
和id2
在图中是否连通。id
进行查找,如果使用List
存储会极大增加查找开销,因此使用HashMap
,id
作为Key,person
作为Value,存储熟人使用person
作为Key,value
作为Value。queryNameRank
方法直接采用遍历的方式计算rank,维护一个排序的容器会增大addPerson
的开销,得不偿失。isCircle
方法判断两点是否连通,使用广度优先搜索(BFS)算法,依靠Java自带的Queue
接口即可实现,难度不高。circleCache
在BFS过程中进行连通性缓存,但由于查找次数太少,缓存策略反而增加了时间开销,得不偿失。NetWork
方法分析加入了组的概念,即子图。
addGroup(Group group)
:添加一个子图。getGroup(int id)
:获取图中编号为id
的子图。addtoGroup(int id1, int id2)
:向子图id2
添加点id1
。queryGroupSum()
:子图数量。queryGroupPeopleSum(int id)
:子图id
中的点数。queryGroupRelationSum(int id)
:子图id
中的边数量的2倍,加上点的总数。queryGroupValueSum(int id)
:子图id
中所有边权值和的2倍。queryGroupConflictSum(int id)
:子图id
中所有人character
的异或。queryGroupAgeMean(int id)
:子图id
中所有人age
的平均值。queryGroupAgeVar(int id)
:子图id
中所有人age
的方差。addtoGroup
时,遍历子图中的所有点添加边和边的权值,在addRelation
时,遍历所有子图,判断是否包含指定两点。由于子图上限10个,所以时间开销极低。age
的总和、平方和,调用平均值与方差询问时直接计算,特别注意方差的计算不能直接化简到概率统计的公式,需要从JML描述展开,否则会出现整型变量的乘除运算误差。NetWork
方法分析在上一次基础上,能够删除子图中的点。
queryAgeSum(int l, int r)
:询问age
在l
、r
范围内的人数。delFromGroup(int id1, int id2)
:从子图id2
中将点id1
删除。queryMinPath(int id1, int id2)
:id1
和id2
间的最短路径长度。queryStrongLinked(int id1, int id2)
:id1
和id2
是否同时存在于一个点双连通分量。queryBlockSum()
:图中的连通块个数。borrowFrom(int id1, int id2, int value)
:借钱,金钱守恒,总数为0。queryMoney(int id)
:询问id
现有钱数。int
维护age
的平方和,因为age
最大值为2000,800人的情况下会溢出,可以使用long
或者遍历计算方差的方式,笔者采用了后者,与JML规格描述相一致。money
主要考察对JML的细致阅读,从id2
向id1
借钱。age
范围内人数直接遍历,由于age
范围比人数大,使用其他算法维护得不偿失。ArrayList
存储每个点所连通的点,处于同一连通块的点共享一个容器对象引用。本质为并查集的思想,并且对连通块总数进行维护。
ArrayList
引用相同,不需要修改相关维护变量。ArrayList
引用不同,使用addAll
方法,将size
小的集合向size
大的集合合并,并更新size
小集合的所有id
的并查集为size
大的集合,确保对象引用的共享。HashMap
和ArrayList
进行点的双维护查找。priorityQueue
实现,新建了DijkstraPair
类存储结点编号与当前最短路径情况,实现Comparable
接口。为了增加访问性能,使用了数组存储最短路径值,每次查找使用Arrays.fill
方法对数组赋予Integer.MAX_VALUE
初始值,但事实上性能略逊于不初始化的空HashMap
。Edge
压入栈中处理,同样使用数组增加访问效率。JML规格中约定了2点的点双不算在范围内,因此特判。一些作业中使用到的细枝末节处理,对整体性能影响很小。
HashMap
的三种遍历方式keySet
,每次使用get
方法获取Value。entrySet
,可以直接获取Key与Value,且遍历效率最高。values
,直接获取Value值,遍历效率最低。HashMap
的查找containsKey
:复杂度\(O(1)\),最坏情况\(O(n)\)。containsValue
:复杂度\(O(n)\)到\(O(n^2)\)之间,所有Value都分布于单独Key时为\(O(n)\)。笔者第九次作业误使用了containsValue
方法,导致CPU时间略高。
HashMap
的put
方法,put
方法存在一定复杂度,基于HashMap
的HashSet
add
方法同理。ArrayList
的遍历效率高于HashSet
,因此共享容器使用了ArrayList
。ArrayList
效率略快于使用foreach
遍历。Arrays.fill
方法类似于C语言中的memset
,用于对数组的初始化,但实际可以使用空的HashMap
实现最短路径的记录。isLinked
询问两点连通时,一边对已有熟人遍历一边判断是否连通自己,在没有熟人时跳过了自连通判断,直接返回了false,随机数据下屡次复现。value
和的数据,发现两个超时Bug。isCircle
超时的Bug。long
,且在计算方差时没有将第二项进行强制类型转换,导致第二项结果为int
且溢出。该Bug由于互测数据数量的限制无法hack,同样是手动构造发现。笔者很不幸在本单元第二次实验的唯一一次补交机会中出现了编译错误的情况,这也是笔者这学期第一次出现编译错误,就是如此的巧合——查询错误根源,是笔者的单元测试中出现了手滑打错自动导入的Java Oracle且被IDEA默认折叠。
百密一疏,但这其实是在警醒笔者CheckStyle的重要性,发现无用导入报错,不论是作业还是实验,甚至于今后的工作,都应当做好代码风格的检查。
笔者建议评测机开放一个测试CPU的窗口,只提供输入和运行服务,设置使用CD。
由于笔者CPU主频与其他dalao相差甚远(测Tarjan超时时疯狂咆哮),在第十次作业本地测试时认为算法实现存在一些难以发现的错误,后发现是CPU差异所致。高频CPU也不一定与评测机相一致,因此希望有个统一的标准来检查程序运行的时间是否符合预期并相应作出优化。
第三单元笔者也有所收获。
同时存在一些需要改进的地方。
另对JML有些主观的评价:JML虽然对规格进行了约束,但是书写JML比书写代码更为复杂,且不易理解过于复杂的JML逻辑,有些本末倒置的感觉。JML的工具链非常不成熟,且无人维护,网络上的JML信息大量来自于往年的OO博客,说明JML本身也没有得到普及。
很感谢老师助教们的辛勤付出,给笔者带来了良好的课程体验,并且及时解决笔者的问题与困难。OO课程到了第三单元的确存在不成熟、不完美的地方,需要时间来不断改进,笔者希望今后的OO能够更好。
标签:失误 请求 输入参数 配置 -- 异或 注意 orm 实例
原文地址:https://www.cnblogs.com/forever518/p/12924641.html