TOP

北航OO(2020)第三单元博客作业(一)
2020-05-20 06:12:48 】 浏览:23次 本网站的内容取自网络,仅供学习参考之用,绝无侵犯任何人知识产权之意。如有侵犯请您及时与本人取得联系,万分感谢。
Tags:北航 2020 第三单元 博客 作业

北航OO(2020)第三单元博客作业

JML语言总结

理论基础

JML是用于对Java程序进行规格化设计的一种表示语言,它使用JavaDoc注释的方式来表示规格。JML以Java语法为基础并进行了一定的扩充。JML的语法分为几个层次,下面对JML Level 0的核心特性进行简要的总结。

规格变量的声明

规格变量分为静态规格变量和实例规格变量两种。以整型数组为例,它们分别可以声明为//@public static model non_null int []elements//@public instance model non_null int []elements

常用表达式

表达式 含义
\result 非void类型的方法的返回值
\old(expr) 一个表达式expr在相应方法执行前的取值(遵从引用规则)
\not_assigned(x, y, ...) 括号中的变量是否在方法执行过程中未被赋值
\not_modified(x, y, ...) 限制括号中的变量在方法执行期间的取值未发生变化
(\forall T x; R(x); P(x)) 全称量词,表示满足R(x)的x都满足P(x)
(\exists T x; R(x); P(x)) 存在量词,表示存在满足R(x)的x满足P(x)
(\sum T x; R(x); expr) 对于满足R(x)的x,求expr的和
(\max T x; R(x); expr) 对于满足R(x)的x,求expr的最大值
(\min T x; R(x); expr) 对于满足R(x)的x,求expr的最小值
<==> 等价操作符
==> 蕴含操作符
\nothing 空集

方法规格

方法规格分为正常行为规格和异常行为规格两种,分别对应normal_behaviorexceptional_behavior。多个规格之间使用also连接。每种规格又可分为前置条件、副作用范围限定和后置条件,分别对应requiresassignableensures。多个子句之间为合取关系。

对于纯粹访问性的方法,即不会对对象的状态进行任何改变,也不需要提供输入参数,这样的方法无需描述前置条件,也不会有任何副作用,且执行一定会正常结束。对于这类方法,可以使用简单的(轻量级)方式来描述其规格,即使用pure关键词。在方法规格中,前置条件可以引用pure方法返回的结果。

对于异常行为规格,我们通常会使用signals或signals_only子句来抛出异常。signals子句的结构为signals (***Exception e) expr;意思是当expr 为true 时,方法会抛出括号中给出的相应异常e;signals_only子句的结构为signals_only ***Exception;,意思是一旦进入此子句,就会抛出相应的异常。

类型规格

类型规格指针对Java程序中定义的数据类型所设计的限制规则,一般而言,就是指针对类或接口所设计的约束规则。课程中的重点是不变式invariant和状态变化约束constraint。不变式invariant是要求在所有可见状态下都必须满足的特性,而状态变化约束constraint对对象状态的变化进行约束。

应用工具链情况

JML的工具链较不完善,且大都已很长时间没有维护。常用的JML工具主要有OpenJML(对JML进行语法检查、配合Solver进行简单的静态验证、以及运行时验证)、JMLUnitNG(自动化单元测试生成工具)和JMLUnit(类似前者)等。OpenJML有Eclipse插件版,使用体验较好。但是没有可用的IDEA插件是一个遗憾。

在http://www.eecs.ucf.edu/~leavens/JML//download.shtml这个页面上,有更多JML相关工具的介绍。

OpenJML验证情况

由于后两次作业无法通过OpenJML的语法检查,下面以第一次作业为例,演示OpenJML的验证。

Parsing and Type-checking

本功能主要检查JML规格的语法。

在IDEA的External Tools中,运行如下命令:java -jar openjml.jar -check "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8,即可进行JML的静态语法检查。-check参数指定检查类型为Parsing and Type-checking,-cp和-sourcepath命令用于指定Classpath和源文件目录,-encoding参数用于指定文件编码。

第一次作业的JML规格成功通过了该检查,返回值为0。

Extended Static Checking

本功能主要利用Solver对按照JML编写的程序进行简单的静态检查。

在IDEA的External Tools中,运行如下命令:java -jar openjml.jar -prover z3_4_7 -exec ".\Solvers-windows\z3-4.7.1.exe" -esc "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8,即可进行JML的静态语法检查。-prover参数用于指定Solver类型,-exec参数用于指定Solver可执行程序,-esc参数指定检查类型为Extended Static Checking。

在对MyPerson检查的过程中,触发了36个警告,其中主要是The prover cannot establish an assertion,但这些警告似乎并不是由于程序的错误,而是Solver无法对程序进行充分的解析导致的;在对MyNetwork检查的过程中,触发了100个警告,其中主要仍是The prover cannot establish an assertion,且提示静态检查不支持对\not_assigned表达式进行检查。由此可见,该功能对一些较为复杂的程序的支持还十分欠缺。

下面展示部分MyPerson类的检查结果:

.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:82: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spe

请关注公众号获取更多资料


北航OO(2020)第三单元博客作业(一) https://www.cppentry.com/bencandy.php?fid=97&id=289063

首页 上一页 1 2 3 4 5 下一页 尾页 1/5/5
】【打印繁体】【投稿】【收藏】 【推荐】【举报】【评论】 【关闭】 【返回顶部
上一篇服务注册、发现、心跳 下一篇微服务的版本选择思考与总结

评论

验 证 码:
表  情:
内  容: