Java知识分享网 - 轻松学习从此开始!    

Java知识分享网

Java1234官方群25:java1234官方群25
Java1234官方群25:838462530
           Java最新职位

GIT视频教程(结合github,码云)免费领取

SpringBoot打造全栈在线教育平台实战课程

毕设代做论文包查重联系人QQ:1982956321毕设大神

66套java实战课程无套路领取

Java1234 VIP课程

领取微信扫码登录Java实现视频教程

Java1234至尊VIP(特价活动)
当前位置: 主页 > Java文档 > Java基础相关 >

JML Level 0手册 PDF 下载


分享到:
时间:2020-05-23 08:57来源:http://www.java1234.com 作者:小锋  侵权举报
JML Level 0手册 PDF 下载
失效链接处理
JML Level 0手册 PDF 下载

下载地址:

提取码: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 }; /
 
------分隔线----------------------------
锋哥公众号


锋哥微信


关注公众号
【Java资料站】
回复 666
获取 
66套java
从菜鸡到大神
项目实战课程