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 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 Spezifikationen von Funktionen präzise auszudrücken.
Die Verwendung von solchen Metasprachen und Beweisen wird sich in der Regel nur für sicherheitskritische Systeme (z. B. Eisenbahnübergänge, Kernkraftwerke) rentieren, da die Beweise sehr aufwendig und damit teuer sind.
Literatur
- "The Vienna Definition Language", P. Wegner, ACM Comp Surveys 4(1):5-63 (Mar 1972).
- D. Bjørner and C. B. Jones (eds.), The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science, Vol. 61, Springer-Verlag 1978. ISBN 0-387-08766-4
- D. Bjørner and 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)