Derivation of axiomatic definitions of programming languages from algorithmic definitions

Abstract

Language definitions by abstract interpreters are appropriate to the design and development of a language. Axiomatic definitions are more appropriate to proving program properties and verification of compilers. The proof methods of Manna and Ashcroft can be applied to an algorithmic definition in, e.g. The Vienna Definition Language to deduce theorems which constitute an axiomatic definition of precisely the same language. The process and techniques are explained, and illustrated on a simple language of assignment statements.