Tools for Testing Denotational Semantic Definitions of Programming Languages.
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
Pagination or Media Count:
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.
- Computer Programming and Software