Vienna Definition Language
aus Wikipedia, der freien Enzyklopädie
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 Computersoftware mit einer Operationalen Semantik anzugeben. Sie stellt eine Metasprache (formale Sprache) dar und wurde u.a. 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 auszudrucken.
Die Verwendung von solchen Metasprachen und Beweisen wird sich in der Regel nur für sicherheits-kritische Systeme (z.B. Eisenbahnübergänge, Kernkraftwerke und andere Echtzeit-Anwendungen) rentieren, da die Beweise sehr aufwendig und damit teuer sind.
[Bearbeiten] Siehe auch
- "The Vienna Definition Language", P. Wegner, ACM Comp Surveys 4(1):5-63 (Mar 1972).
- D. Bjorner, C.B. Jones "The Vienna Definition Method - The Metalanguage" in Bjorner, D. et al eds, "The Vienna Development Method: The Meta- Language", LNCS 61, Springer 1978.
- P. Lucas, "Formal Semantics of Programming Languages: VDL," IBM J. Res. Develop. 25,549-561 (1981)
