Executable specification of static semantics

Abstract

In this paper we have presented three main ideas:Semantic specifications written using inference rules may be executed. The method may be compared with the approach taken in the SIS system of Peter Mosses [Mos78].A Prolog system is adequate for executing such a specification.Intensive use of overloading make semantic specifications easier and more elegant. Typol seems to be a very intuitive way to introduce semantic specifications into a system like Mentor. We would like to use more of Prolog's power (back-tracking for example) to specify the static semantics of programming languages with overloading, such as Ada. Other examples will be needed to improve the Typol formalism and to see exactly what its limits are, both from a theoretical and a practical standpoint.