Tools for Testing Denotational Semantic Definitions of Programming Languages.
Abstract
A denotational formal sematic defintion (FSD) of the Ada programming language was developed at the Institut National de Recherche en Informatique et en Automatique (INRIA), in France. Its intent is to provide the precise meaning of the language and its constructs via the mathematical formalism which underlies the denotationa semantic descriptive technique. Due to the complexity, it is difficult for a person to understand the definition or to attempt symbolic execution of the definition without machine assistance. This report describes the work of the ISI Formal Sematics project in developing and constructing tools to aid the understanding and validation of the ADA FSD. First we briefly describe the INRIA meta-language, AFDL, and the extensions we were forced to make to it. Next we describe the various tools we have built and their application to the interpreting of the FSD. Finally, we describe the outcome of the project. The appendices contain an informal specification of our enhanced version of AFDL (AFDL +), a definition of the toy programming lanuage TINY in ADFL +, and a transcript of an example use of our tools to process TINY definition.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1983
- Accession Number
- ADA129818
Entities
People
- Allen Stoughton
- David F. Martin
- Vittal Kini
Organizations
- University of Southern California