1 JML 语言的基础及应用
1.1 JML 语言
Java 建模语言 (JML) 是一种行为行为规范语言, 可以使用给定 Java 模块的行为. 为了支持 JML 语言的轴论, 我们将 Eiffel 的 "合同设计(contract design)" 方法与 Larch 系列框架规范语言的基于模型的规范方法相结合. 主要文章为以下三篇文章. 一些要素.
1.2 JML 语言相关工具
The AspectJML tool: 为 Java 和 AspectJ 做运行时检查的工具
The jml4c tool: 基于 Eclipse Java 编译器开发的 JML 语言编译器
Sireum/Kiasan for Java: 一个基于契约的自动化验证测试工具
JMLEclipse: 在 Eclipse 的 JDT 编译器基础上开发的 JML 工具包
JMLUnitNG: 自动化测试生成工具
JMLOK: 用随机测试检查 java 代码是否符合 JML 规格并对不一致现象给出可能的原因
jml 是将 java 程序规格化的一种表示语言. jml 主要用于 (一) 开展规格化设计;(二)应对现有的代码使用规格, 增强代码的维护性, 维修性.
需要注意的是: jml 将显示我们的流程在什么情况下能够正确执行, 预期的回调价格能够满足什么条件, 用一句话来说,
jml 是流程可以以什么原料执行的. 不是告诉你烹饪方法, 而是出什么菜. 这也是笔者所犯的典型错误.
接下来总结一下 jml 中常见的表现方式:
\result 表示一个回程价格不是 void 方法实施后的回返值.
\old(expr)表现式 expr 在实施该方法之前会收取费用.
\not_assigned(x,y,...)表示括号内的变数在执行过程中是否附加, 但在实际使用中, 经常在后置条件下, 对括号内的变数进行约束
\forall 全称量语, 实际使用与 for 循环类似(\forall xx ; xx)
\exists 存在量单词, 实际使用及 \ forall 类似 回到给予的范围内, 表达方式的和.
\sum int i ; 0 <= i & i <= 5 ; i, 结果 15 回到
\product 周期范围, 表现式伦达鲁克敌, 使用类似于 \ sum.
\max & \min 是回归到订购范围表现式的最大 (最小) 值.
requiress 方法的前提条件是, 万只有在脚前置条件的情况下, 方法才能正确地执行, 因此, 要求采购人正确地履行前置条件.
ensures 方法的后置条件, 方法保证实施完成后的结果, 满足后置条件的约束.
assignable 副作用, 即在方法实施过程中允许或对某些变数进行修改.
signals 投的球数超过了规定数.
2 心得体会
由于我没法完成这单元的作业, 就整理了一下 JML 的内容和概要,
我觉得规格是 OO 的一种很好的体现, 要熟悉写规格的语法, 准确的规格利于以后对程序的测试与维护.
对于规格的学习对未来的大项目开发, 团队编程会有很大的帮助, 所以要继续学习
来源: http://www.bubuko.com/infodetail-3776012.html