jml以javadoc注释的方式来表示规格,每行都以@起头。
//@annotation
/* @ annotation @*/
jml的表达式是对java表达式的扩展,新增了一些操作符和原子表达式。
expr
)表达式:用来表示一个表达式expr
在相应方法执行前的取值。针对一个对象引用而言,只能判断引用本身是否发生变化,而不能判断引用所指向的对象实体内容是否发生变化。true
,否则返回false
。container
)表达式:表示container
对象中存储的对象不会有 null。type
)表达式:返回类型type
对应的类型(class)。expr
)表达式:该表达式返回expr
对应的准确类型。e1<:e2
,如果类型e1是类型e2的子类型(sub type),则该表达式的结果为真,否则为假。如果e1和e2是相同的类型,该表达式的结果也为真。b_expr1<==>b_expr2
或者b_expr1<=!=>b_expr2
,其中b_expr1
和b_expr2
都是布尔表达式,这两个表达式的意思是b_expr1==b_expr2
或者b_expr1!=b_expr2
。b_expr1==>b_expr2
或者b_expr2<==b_expr1
。对于表达式b_expr1==>b_expr2
而言,当b_expr1==false
,或者b_expr1==true
且b_expr2==true
时,整个表达式的值为true
。assignble
表示可赋值。modifiable
则表示可修改。signals (exception e) b_expr
:当b_expr
为true
时,方法会抛出括号中给出signals_only
:后面跟着一个异常类型,不强调对象状态条件,强调满足前置条件时抛出相应的异常。一开始想对path中的一些简单方法进行测试,但是报了很奇怪的错误,也不懂如何解决,遂放弃。
于是我手写了一个简单的测试程序test.java,其功能是非负数的加法,且未对溢出情况做处理。
package test; public class test { //@ public normal_behavior //@ requires a >= 0 && b >= 0; //@ ensures \result == a + b; public static int sum(int a, int b) { return a + b; } public static void main(string[] args) { sum(1, 2); } }
初始目录结构如下:
test └── test.java
执行java -jar jmlunitng.jar test/test.java
test ├── packagestrategy_int.java ├── packagestrategy_java_lang_string.java ├── packagestrategy_java_lang_string1darray.java ├── test.java ├── test_instancestrategy.java ├── test_jml_data │ ├── classstrategy_int.java │ ├── classstrategy_java_lang_string.java │ ├── classstrategy_java_lang_string1darray.java │ ├── main__string1darray_args__10__args.java │ ├── sum__int_a__int_b__0__a.java │ └── sum__int_a__int_b__0__b.java └── test_jml_test.java
执行javac -cp jmlunitng.jar test/*.java
test ├── packagestrategy_int.class ├── packagestrategy_int.java ├── packagestrategy_java_lang_string.class ├── packagestrategy_java_lang_string.java ├── packagestrategy_java_lang_string1darray.class ├── packagestrategy_java_lang_string1darray.java ├── test.class ├── test.java ├── test_instancestrategy.class ├── test_instancestrategy.java ├── test_jml_data │ ├── classstrategy_int.class │ ├── classstrategy_int.java │ ├── classstrategy_java_lang_string.java │ ├── classstrategy_java_lang_string1darray.class │ ├── classstrategy_java_lang_string1darray.java │ ├── main__string1darray_args__10__args.class │ ├── main__string1darray_args__10__args.java │ ├── sum__int_a__int_b__0__a.class │ ├── sum__int_a__int_b__0__a.java │ ├── sum__int_a__int_b__0__b.class │ └── sum__int_a__int_b__0__b.java ├── test_jml_test.class └── test_jml_test.java
执行java -jar openjml.jar -rac test/test.java
执行java -cp jmlunitng.jar test.test_jml_test
测试结果:
[testng] running: command line suite passed: racenabled() passed: constructor test() passed: static main(null) failed: static sum(-2147483648, -2147483648) passed: static sum(0, -2147483648) passed: static sum(2147483647, -2147483648) passed: static sum(-2147483648, 0) passed: static sum(0, 0) passed: static sum(2147483647, 0) passed: static sum(-2147483648, 2147483647) passed: static sum(0, 2147483647) failed: static sum(2147483647, 2147483647) =============================================== command line suite total tests run: 12, failures: 2, skips: 0 ===============================================
可以看到自动生成的测试用例采用的是极端数据的组合,对于负数以及溢出都显示failed表明未通过测试,这与我们的预期相符。
第一次作业比较简单,只有对路径的增删查改等基本功能,仅需实现path
和pathcontainer
两个容器类再加上一个主类即可,实现的时候根据jml按部就班地写就没什么问题。唯一要注意的一点是时间复杂度的问题,因为查询指令很多,使用hashmap
和hashset
是一个较好的选择,能基本保证o(1)的复杂度。
从这次作业开始涉及到图结构,增加了判断容器中是否存在某个结点、容器中是否存在某一条边、两个结点是否连通以及计算两个结点之间的最短路径的方法。
对于结点我使用hashmap
存储,以结点id为值,重复个数为键。对于边我采用的是嵌套的hashmap
,由结点再映射到一个hashmap
,内容是与它连接的结点及其重复个数。这样,就能把图结构完整的保存下来,查询效率高,同时也易于增删维护。
对于连通性和最短路,我采用了bfs,遍历的过程中会用到一个weightednode
类,用来保存源点到当前节点的最短路径长度,并传递给下一个节点累加使用。此外,我还用shortestpath
类来描述已经算出的最短路,它包含两个节点的信息,并重写了equals()
和hashcode()
,从而可以保存在hashmap
中作为最短路的缓存。值得一提的是,a -> b
和b -> a
的最短路是一样的,在重写以上两个方法时要注意对称性。
本次作业需要实现一个动态的地铁系统。从类图中的继承关系可以看出,这三次作业是一脉相承、逐次递进的,模拟了实际oop开发中一个功能模块的演化过程。
在保留了上次作业的大体架构的基础上,引入multinode
来描述在不同路径上具有相同id的结点,这是因为我采用的是"拆点"的建图方法,需要区分这些重复的结点。此外,用pair
类代替并扩展了shortestpath
类,使其可以同时描述最短路路径、最低票价、最少换乘次数、最少不满意度多种两点结构。算法上采用dijkstra算法,在每次查询时计算出源点到其所在连通块的所有节点的最低票价/最少换乘次数/最少不满意度,并存入缓存以便下次直接使用。至于最短路和连通块,依然是用bfs进行计算。
本次作业主要有两方面的不足:
三次作业均用对拍进行测试。
可能是因为比较简单,没有被测出bug,也没有测出别人的bug。
依然没有测出或被测出bug。
提交前就在担心会不会因为拆点复杂度过高而超时,结果果然惨不忍睹,未通过的点都是因为tle。目前正在bug修复阶段,考虑换一种建图的方法。
本单元主要学习jml规格,具体来说包含两方面的内容:根据需求撰写规格,以及根据规格实现代码。jml是基于"契约式编程"的一种规格描述语言,相比于自然语言注释,jml更加严谨和清晰。只要能保证规格本身是满足需求的,并且编程时严格按照规格实现,理论上就程序就一定是正确的。在这种情况下,即使出现了bug,也能通过openjml、jmlunitng等工具自动化地定位问题所在。
但jml也有美中不足的地方,比如学习成本高,读起来没有自然语言那么易于理解。尤其是撰写规格是一件极其费时费力的工作,其难度不亚于代码实现本身。可能在工业界,尤其是那些不容许任何程序错误的场景下(如航空航天、军事领域),使用jml是一种较好的易于沟通和协作的编程方式,且能在最大程度上避免错误的产生。但在小团队的常规开发中,私以为自然语言会是相对更好的选择。
然而无论如何,jml是一门值得了解和学习的技术。
如对本文有疑问, 点击进行留言回复!!
Java面向对象中:方法重载和方法重写以及区别、 this关键字和super关键字以及区别
网友评论