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 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-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)
Content Disclaimer
Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.
- The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
- There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
- It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
- Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
- Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.