Strategies of Modeling from VDM-SL to 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 of the design are illustrated with an example.