Vienna Definition Language

The Vienna Definition Language ( VDL ) is a programming language developed in the IBM laboratory in Vienna that can be used to specify formal, algebraic definitions of programming languages ​​for software with operational semantics . It provides a meta-language ( formal language ) is and has been used, among other things, to the programming language PL / I to be defined.

A methodology, Vienna Development Method , was developed from the language , which makes it easier to formulate and maintain correctness proofs using computer programs. It uses mathematical notation to precisely express specifications of functions .

The use of such metalanguages ​​and evidence will usually only pay off for safety-critical systems (e.g. railroad crossings, nuclear power plants), as the evidence is very complex and therefore expensive.

literature

• "The Vienna Definition Language", P. Wegner, ACM Comp Surveys 4 (1): 5-63 (Mar 1972).
• D. Bjørner and CB 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 CB 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)