Vienna Development Method

The Vienna Definition Language (VDL ) is a technology developed at the IBM Laboratory in Vienna programming language that can be used to specify formal, algebraic definitions of programming languages ​​for computer software with an operational semantics. It is a metalanguage ( formal language ), and was used inter alia in order to define the programming language PL / I.

Also a methodology Vienna Development Method has been developed, which makes it easier to formulate correctness proofs about computer programs and to run out of language. It uses a mathematical notation to express specifications of functions precisely.

The use of such meta-languages ​​and proofs will be profitable usually only for safety-critical systems (eg railroad crossings, nuclear power plants ), because the evidence is very complex and therefore expensive.