面向对象第三单元总结 unit3
作者：互联网
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的一种很好的体现，要熟悉写规格的语法，准确的规格利于以后对程序的测试与维护。
对于规格的学习对未来的大项目开发，团队编程会有很大的帮助，所以要继续学习
标签：Java,JML,面向对象,规格,jml,unit3,方法,单元,语言 来源： https://www.cnblogs.com/ManGoStin/p/14830021.html