链接：https://pan.baidu.com/s/17B0KNTXt5V4HV976OCj37Q 

提取码：hq3x

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口

规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对

方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在

Larch上的工作，并融入了Betrand Meyer， John Guttag等人关于Design by Contract的研究成果。近

年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不

仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满

足情况。

一般而言，JML有两种主要的用法：

（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻

辑严格的规格。

（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面

具有特别重要的意义。

JML的设计考虑到了未来扩展需要，把语言分成了几个层次。其中level 0是最核心的语言特征，要求所

有的JML工具都要支持。从课程教学角度，我们仅针对level 0语言特征，选择其中最核心和最常用的一

些要素进行介绍和训练。建议同学们通过http://www.jmlspecs.org/来了解更多细节。

1. 注释结构

JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注

释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。按照Javadoc习惯，JML

注释一般放在被注释成分的紧邻上部，如下面的例子所示。其中有效的Java代码为line1, line 3, line

15，line18和line19。 package org.jmlspecs.samples.jmlrefman; // line 1 // line 2 public abstract class IntHeap { // line 3 // line 4 //@ public model non_null int [] elements; // line 5 // line 6 /*@ public normal_behavior // line 7 @ requires elements.length >= 1; // line 8 @ assignable \nothing; // line 9 @ ensures \result // line 10 @ == (\max int j; // line 11 @ 0 <= j && j < elements.length; // line 12 @ elements[j]); // line 13 @*/ // line 14 public abstract /*@ pure @*/ int largest(); // line 15 // line 16 //@ ensures \result == elements.length; // line 17 public abstract /*@ pure @*/ int size(); // line 18 }; /