第三单元作业总结
18373330 张洪康
JML语言的理论基础
- Java Modeling Language(JML)是一种java的规格描述语言,描述java类中各方法模块的行为,实现对java程序进行规格化设计的目的。
- JML允许在规格中混合使用Java语法成分和JML引入的语法成分
- JML语言是逻辑语言,无二义性,便于团队之间交流和理解模块的功能。
- JML语言通过验证运行结果描述模块的功能,而不必描述中间过程的具体实现。
- 一般而言,JML由标题,前置条件,副作用,后置条件等组成。
JML语法与工具链
- JML 语法一览
- Precondition • /@ requires P; @/ •
- Postcondition • /@ ensures P; @/ •
- Side-Effects • /@ assignable list;@/ •
- Exception • /@ signal (Exception e) P;@/ •
- Invariant • /@ invariant P; @/ •
- Constraint • /@ constraint P; @/ •
- method result reference • esult • Previous expression value • old(E)
- JML工具链
- openJML
JUNIT测试
进行了部分测试但还是没测到BUG(因为手搓测试所以JML读错了测试数据也是错的QAQ)
作业架构分析
由于课程组每个方法都给出了JML,所以具体实现上殊途同归。
- 第一次作业
由于这次作业比较基本,且性能没有差距,给啥无脑写啥就行。 - 第二次作业
有了一些性能分的影响,但基本上还算比较简单,将第一次作业中的ArrayList等性能影响较大的容器改为了Hashmap等查找O(1)的容器。 - 第三次作业
在强连通上比较考验性能优化,其他与之前没有太大差异。
BUG分析
-
第一次作业
无 -
第二次作业
由于JML读疏忽,导致在RANK的方法上“按名称排名”的方法写成了”按id排名“,虽然采用了二分查找的方法,但只得了15分QAQ。 -
第三次作业
强测上有几个点TLE(QSL),在优化算法之后通过。
心得体会
-
耐心读完JML
-
有时间的话对每个方法进行充分的测试
-
不会用工具链QAQ
-
目前读懂JML问题不大,可能在实践中还不能写出来。
-
JML虽然严格控制了每一个方法的输入输出规格,但也不是说确保了每一个方法的正确性以及性能就可以达到总体的要求和高性能。由于JML没有给定实现方法,其在具体实现中,比如容器等的选择上会导致一个类中涉及到这些的部分千差万别,导致最后总体设计出来的程序在性能上有较大差异。所以即使面对已经设计好的JML,在实现时也需要”统筹全局“,比如数据容器、是否需要新增其他类、预处理以提高性能等等。比如因为某一个方法有查询功能就直接无脑Hashmap而忽略掉其他方法可能涉及到的排序等。