维也纳方法简论

维也纳开发方法(VDM)就是在维也纳学派的标志语义、证明逻辑等理论研究基础上形成的切实可行的软件开发方法.本文从实际应用的角度讨论了VDM如何处理程序开发过程的形式化方面:怎样从系统的高度形式化的规范说明按步就班地开发出高级语言程序.同时还讨论了建立软件开发环境以实践VDM的方法.

维也纳分析方法及其应用

介绍了软件开发方法中的一种形式化分析方法:ViennaDevelopmentMethod(VDM)。阐述了形式化分析方法的特点,具体说明了维也纳分析方法规格说明的两种规范:模块化说明与非模块化说明,及程序证明性依据:基于函数与操作的形式化规格说明。然后通过一个应用实例来说明如何利用VDM技术进行软件开发,及利用函数与操作的形式化规格说明来证明程序是正确的。

UML类模型的VDM++形式化规约

利用目前使用最为广泛的形式化验证语言VDM++在描述系统模型的语法和语义上的精确、一致的特点,结合VDMTOOLS和Rational Rose工具把UML类模型中的各个元素转化成VDM++表示,从而实现对UML类模型中所包含的各个元素进行语法和语义的检查。进一步提高UML的建模质量。