JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。它是一种行为接口规格语言(BISL),基于Larch方法构建,特别为Java定制。JML的基本用途是描述Java模块方法的形式规范,它以注释的形式出现在Java源文件中,但并没有与代码分离。这些形式规范在Java文件编译时不会影响代码的编译执行。
JML具有以下几个特点:
- 无二义性:JML是逻辑语言,无二义性,便于团队之间交流和理解模块的功能。
- 验证结果:JML通过验证运行结果描述模块的功能,而不必描述中间过程的具体实现,为描述模块功能提供便利。
- 工具支持:JML作为一门比较新的形式规范描述语言,提供了很多工具来描写、检查、甚至自动生成形式规范的基奉框架。例如,STM solver和SMT solver工具可以静态分析代码,检查代码对规格的满足情况。
JML的主要用途包括开展规格化设计,使得交给代码实现人员的不是可能带有内在模糊性的自然语言描述,而是逻辑严格的规格;以及针对已有的代码实现,书写其对应的规格,从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。