page 1  (21 pages)
2to next section

A Tool to Support Formal Reasoning about

Computer Languages?

Richard J. Boulton

University of Cambridge Computer Laboratory

New Museums Site, Pembroke Street

Cambridge CB2 3QG, United Kingdom

November 1996

Abstract

A tool to support formal reasoning about computer languages and specific language texts is described. The intention is to provide a tool that can build a formal reasoning system in a mechanical theorem prover from two specifications, one for the syntax of the language and one for the semantics. A parser, pretty-printer and internal representations are generated from the former. Logical representations of syntax and semantics, and associated theorem proving tools, are generated from the combination of the two specifications. The main aim is to eliminate tedious work from the task of prototyping a reasoning tool for a computer language, but the abstract specifications of the language also assist the automation of proof.

1 Introduction

For several decades theorem proving systems have been used to reason about computer languages. A common approach has been to define the semantics of a language in the logic of the theorem prover. Properties of particular language texts can then be proved. With some approaches it is also possible to prove general properties about the language itself. The technique has been referred to as embedding.

Examples of embedding include an early compiler correctness proof for a simple ALGOL-like language [MW72] mechanised in Stanford LCF [Mil72], Moore's

?Research supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/J42236.