The Language for DENOTE (Denotational Semantics Translation Environment)
AEROSPACE CORP EL SEGUNDO CA ENGINEERING GROUP
Pagination or Media Count:
The State Delta Verification System SDVS is a proof checker for correctness proofs 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 DENOTEDenotational 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.
- Computer Programming and Software