在软件工程中,自然语言描述需求说明文档的做法应用广泛,典型的如使用UML建模工具。但是,自然语言的多义性、上下文有关性、非系统性等特点致使其在描述复杂系统时可能引起语法二义性和系统的不一致性。为了保证软件产品的可靠性,形式化方法应运而生。形式化方法采用形式规约语言精确地描述软件规约说明,建立精确的、无二义性的语义,以数学的精确性保证了系统结构的合理性、正确性和良好的可维护性。VDM是形式化的抽象模型方法中最具代表性的一种。它是一种功能构造性规格说明技术,它的核心元素是其标准化规范语言VDM-SL。数学的精确性使它能够有效地保证系统的设计和开发,因而广泛应用于工业界的形式化系统开发。JML是一种基于Java高级语言的形式的行为接口规范语言,它用来规范Java的模块的行为和具体设计。JML的思想来自于Eiffel语言的契约式设计思想。目前基于JML的验证、调试和测试等支撑工具已经比较成熟。本文分析了VDM-SL和JML这两种抽象层次不同的规范语言,提出了从VDM-SL语言到JML语言在常量、变量以及约束上的转换策略。针对VDM-SL语言语法子集的BNF范式提出了VDM-SL规范到JML约束的转换的设计方案,本文具体地分别描述了基本数据类型、集合操作、用户自定义类型、状态、类型约束、函数和运算等有意义的VDM结构到JML的映射机制。同时,文章给出了基于上述VDM-JML映射机制的工具JML-SL to JML的实现框架。它是一个基于Eclipse平台的插件,用来辅助用户把VDM约束按照已定义好的VDM-JML转换机制映射到相应的带有JML规范注释的Java程序。相应的Java的模块在后续的开发中由开发人员进行实现。程序验证方面,本文利用了JML的测试工具间接地验证了VDM-SL的规范。VDM-JML的转换的策略使得上层设计对下层开发的指导机制更加完善,因而构造了一个贯穿于整个软件生命周期的软件开发方法。通过需求、架构、设计、开发、测试等开发步骤的螺旋迭代,系统的软件原型得以逐步求精,从而使得软件的实现更加契合系统的设计思路。由此,VDM-JML的转换对于改善软件开发的流程、实现顺畅的软件生命周期具有相当重要的意义。