imported>YMS: Sprache, Format

2024-04-17T19:30:59Z

Sprache, Format

Neue Seite

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. 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]]

Vienna Definition Language - Versionsgeschichte

imported>YMS: Sprache, Format