从VDM-SL到JML建模的转换策略
Strategies of Modeling from VDM-SL to JML
VDM是一种广泛应用于工业界的形式化开发方法，数学的精确性使它能够有效地保证系统的设计和开发。JML是基于Java的形式化的行为接口规范语言（BISL），目前基于JML的验证、调试和测试等支撑工具已经比较成熟。本文分析了这两种抽象层次有别的规范语言，提出了从VDM到JML常量、变量以及约束在语法的关系映射机制，得到了VDM规范到JML约束的转换的设计方案，使得上层设计对下层实现的指导机制更加完善，从而构造了贯穿整个软件生命周期的软件开发方法。
VDM-SL is one of the most popular formal language used in software development, its mathematical approach allows unambiguous specification and development of high integrity software. JML is a behavioral interface specification language tailored to Java(TM). And the existing JML-based tools of debugging, verifying and testing are mature. This paper discusses the two kinds of specification language and provides a novel design mapping VDM-SL to JML of constant values, variables and constraints. The strategies are illustrated with an example.
靳丹、杨宗源
计算技术、计算机技术
VDM-SLJMLBC形式化软件开发
VDM-SLJMLDBCformal methodsoftware engineering
靳丹,杨宗源.从VDM-SL到JML建模的转换策略[EB/OL].(2008-06-03)[2025-08-17].http://www.paper.edu.cn/releasepaper/content/200806-47.点此复制
评论