The Language for DENOTE (Denotational Semantics Translation Environment)

Abstract

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 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 31, 1990
Accession Number
ADA237144

Entities

People

  • J. V. Cook

Organizations

  • The Aerospace Corporation

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Bits
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Environment
  • High Level Languages
  • Instruction Set Architecture
  • Language
  • Lisp Programming Language
  • Programming Languages
  • Specifications
  • Translations
  • Verification

Fields of Study

  • Computer science

Readers

  • Analytical Mechanics
  • Computational Linguistics