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.