Quelltext der Seite Vienna Definition Language

Die ''' Vienna Definition Language''' ('''VDL''') ist eine im [[IBM]]-Labor in [[Wien]] entwickelte [[Programmiersprache]], die verwendet werden kann, um formale, algebraische Definitionen von Programmiersprachen für [[Software]] mit einer [[Operationelle Semantik|Operationellen Semantik]] anzugeben. Sie stellt eine [[Metasprache]] ([[formale Sprache]]) dar und wurde unter anderem verwendet, um die Programmiersprache [[PL/I]] zu definieren. 

Aus der Sprache heraus wurde auch eine Methodologie, [[Vienna Development Method]], entwickelt, die es erleichtert, Korrektheitsbeweise über Computerprogramme zu formulieren und zu führen. Sie verwendet eine mathematische Notation, um [[Spezifikation]]en von [[Funktion (Programmierung)|Funktionen]] präzise auszudrücken. 
 
Die Verwendung von solchen Metasprachen und Beweisen wird sich in der Regel nur für sicherheitskritische Systeme (z.&nbsp;B. Eisenbahnübergänge, Kernkraftwerke) rentieren, da die Beweise sehr aufwändig und damit teuer sind.  

== Literatur ==
* "The Vienna Definition Language", P. Wegner, ACM Comp Surveys 4(1):5-63 (Mar 1972).
* [[D. Bjørner]], [[C. B. Jones]] (Hrsg.): ''The Vienna Development Method: The Meta-Language'', [[Lecture Notes in Computer Science]], Vol. 61, [[Springer Science+Business Media|Springer-Verlag]] 1978. ISBN 0-387-08766-4
* D. Bjørner, C. B. Jones: ''Formal Specification and Software Development'' [[Prentice Hall]] International, 1982. ISBN 0-13-880733-7
* P. Lucas: "Formal Semantics of Programming Languages: VDL," IBM J. Res. Develop. 25,549-561 (1981)

[[Kategorie:Programmiersprache]]