Language for DENOTE (Denotational Semantics Translation Environment)

摘要

The State Delta Verification System (SDVS) is a proof checker for correctnessproofs of properties expressed in the state delta logic. When one proves correctness properties of a computer program within SDVS, one must first translate the program into the language of the state delta logic. The translation semantics of a computer language can be specified formally by means of denotational semantics. In this report we describe an automated environment for specifying and implementing denotational semantics, called DENOTE(Denotational Semantics Translation Environment). The language accepted by DENOTE is called the DENOTE language (DL). DL is a language in which formal denotational semantic specifications can be written. DL specifications can be transformed by DENOTE into text suitable for input to the Scribe and LaTEX formatters, as well as into Common Lisp code that implements the specified semantics.