Publication
ACM Conference on Proving Assertions about Programs 1972
Conference paper

Derivation of axiomatic definitions of programming languages from algorithmic definitions

Download paper

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.

Date

Publication

ACM Conference on Proving Assertions about Programs 1972

Authors

Topics

Resources

Share