Vienna Development Method

2017-12-21 14:13

在 lua源码欣赏中,提到了 lua 的作者 Roberto 在设计 lua 时的部分灵感来源于 VDM,而关于 VDM 的中文资料却很少。在这里提供一个简单的中文版本备忘。

Wiki原文 https://en.wikipedia.org/wiki/Vienna_Development_Method

维也纳开发法 (VDM) 是历史最悠久的计算机系统开发的 形式方法 [1] 之一。其原型是在20世纪70年代于 IBM 维也纳实验室完成的,后来 VDM 成为了一门基于 VDM-SL (VDM Specification Language) 的一系列技术和组件的形式规范化语言。VDM 还有扩展的形式: VDM++。VDM++ 支持面向对象和并发系统。对 VDM 的支持包括商业和教育中用于分析模型的工具,还包括模型的测试和验证和由VDM模型生成的程序代码。VDM及其工具在工业应用历史和形式主义研究中不断发展,为关键系统、编译器、并发系统和计算机科学逻辑的工程化做出了显著的贡献。

Philosophy#

在VDM-SL中,计算系统可以在比编程语言实现更高的抽象层次上进行建模,从而可以在系统开发的早期阶段对设计进行分析和确定关键特征和缺陷。已经验证的模型可以通过细化过程转化为详细的系统设计。该语言有一个正式的语义,可以在更高抽象层次上证明模型的属性。 它还有一个可执行子集,使得模型可以通过测试进行分析,并可以通过图形界面展示,以便模型可以由不熟悉建模语言本身的专家进行评估。


  1. https://zh.wikipedia.org/wiki/形式化方法


标签:programming

点击加载Disqus评论
Creative Commons © 2013 — 2018 xiao_cang | Theme based on fzheng.me & NexT | Hosted by Netlify