Executable Operational Semantics of Programming Languages
11:00 a.m., Monday, November 23, 1992
12th floor conference room, 719 Broadway
Since the inception of computer languages there have been attempts to define programming languages formally. Several markedly different methodologies have been proposed to solve this problem. This thesis argues for Executable Operational Semantics (EOS) as a methodology for formal definition which has many fundamental advantages. The EOS methodology has, however, been broadly criticized. We show that the major objections against EOS are unfounded, and that executability is suitable and useful for many applications of formal definitions. The primary criticisms of EOS definitions- that they are hardware and architecture specific, that they are unable to describe concurrency and non-determinism, and that they overspecify implementation details-are countered by the demonstration that Ada/Ed, an executable definition of Ada developed at New York University, can avoid or overcome each problem. A description of the implementation of Ada's real arithmetic and representation specifications reveals hardware and architectural independence in an executable definition. Ada/Ed's model of Ada tasking demonstrates that concurrency can be defined within an executable framework, and we argue that an executable definition can describe all non-deterministic aspects of Ada. The problems of overspecificity can be alleviated by the appropriate choice of metalanguage and software techniques, and by suitable parameterization of the formal definition. Finally, we describe some general advantages of executable definitions. We present worked examples of questions to a formal definition of Ada, and establish that requiring a definition to be executable enhances rather than degrades its usability and credibility.