维也纳开发法

维也纳开发法（VDM）是基于计算机的系统开发中历史最悠久的形式化方法之一。起源于20世纪70年代IBM维也纳实验室的工作，它已经发展到包括一组基于形式化规范语言的技术和工具--VDM规范语言（VDM-SL）。

它有一个扩展形式，即VDM++，它支持面向对象和并发系统的建模。对VDM的支持包括用于分析模型的商业和学术工具，包括支持测试和证明模型的属性，以及从验证的VDM模型生成程序代码。

VDM及其工具在工业上的应用已经有了一定的历史，在形式主义方面的研究越来越多，对关键系统的工程、编译器、并发系统和计算机科学的逻辑学都有明显的贡献。

计算系统可以在VDM-SL中以比编程语言更高的抽象水平进行建模，允许在系统开发的早期阶段对设计进行分析并识别关键特征，包括缺陷。经过验证的模型可以通过细化过程转化为详细的系统设计。

该语言有一个形式化的语义，能够对模型的属性进行证明，以达到高水平的保证。它也有一个可执行的子集，所以模型可以通过测试来分析，也可以通过图形用户界面来执行，所以模型可以由不一定熟悉建模语言本身的专家来评估。

VDM-SL的起源是在维也纳的IBM实验室，该语言的第 一个版本被称为维也纳定义语言（VDL）。VDL主要用于提供操作语义描述，而VDM-Meta-IV则提供指称语义。

"在1972年年底，维也纳小组再次将注意力转向从语言定义中系统地开发一个编译器的问题。所采用的总体方法被称为"维也纳开发法"......实际采用的元语言（Meta-IV）在BEKIČ74中被用来定义PL/1的主要部分（如ECMA74中给出的--有趣的是，这是一份写成抽象解释器的正式标准文件）。

"Meta-IV和Schorre的METAII语言，或其后续的TreeMeta之间没有任何联系；这些是编译器-编译器系统，而不是适合形式化问题描述。所以Meta-IV被用来定义PL/I编程语言的主要部分。

其他使用Meta-IV和VDM-SL回顾性地描述或部分描述的编程语言包括BASIC编程语言、FORTRAN、APL编程语言、ALGOL60、Ada编程语言和Pascal编程语言。

Meta-IV演化成几个变体，一般被称为丹麦、英国和爱尔兰学派。英国学派源于CliffJones在VDM中与语言定义和编译器设计无关的方面的工作。

它强调通过使用从丰富的基础类型集合中构建的数据类型来对持久状态进行建模。功能性通常是通过操作来描述的，这些操作可能对状态有副作用，而且大多是用前提条件和后置条件来隐含地指定。

丹麦学派倾向于强调一种建设性的方法，在更大程度上使用明确的操作规范。丹麦学派的工作导致了第 一个欧洲验证的Ada编译器。该语言的ISO标准于1996年发布（ISO,1996）。

VDM-SL和VDM++的语法和语义在VDMTools语言手册和可用文本中都有详细描述。ISO标准包含了该语言语义的正式定义。在本文的其余部分，使用了ISO定义的交换（ASCII）语法。

有些文本倾向于使用更简洁的数学语法。一个VDM-SL模型是以对数据执行的功能给出的系统描述。它由一系列数据类型的定义和对它们进行的功能或操作组成。

基本类型：数字、字符、标记和引号类型VDM-SL包括基本类型，对数字和字符进行建模，具体如下。

数据类型被定义为代表建模系统的主要数据。每个类型定义都引入了一个新的类型名称，并给出了基本类型或已经引入的类型的表示。例如，一个为登录管理系统建模的用户标识符的类型可能被定义如下。

类型UserId=nat为了操作属于数据类型的值，在这些值上定义了操作符。因此，提供了自然数加法、减法等，以及布尔运算符，如平等和不平等。