Lecture Notes ni Computer Science Edited by G. Goos and .J Hartmanis 42 semaJ .E Donahue Complementary Definitions of Programming Language Semantics galreV-regnirpS .grebledieH-nilreB weN kroY 6791 Editorial Board .P Brinch Hansen • D. Gries • C. Moler • G. Seegm~ller • .J Stoer N. Wirth Author James .E Donahue Cornell University Department of Computer Science Upson Hall Ithaca, N.Y. 14853/USA Library of Congress Cataloging iu Publication Data Donahue, James Edward, 1947- Complementary definitions ofp rogramming language semantics. (Lecture notes in computer science 42) ; Bibliography: .p Includes index. .1 Programming languages (Electronic computers) .2 Pascal (Computer program language) .3 Semantics. .I Title. ,II Series. QA76.7.D66 O01.6'424 Z6-6573 AMS Subject Classifications (1970): 94.50 CR Subject Classifications (1974): 4.22, 5.24 ISBN 3-540-07628-X Springer-Verlag Berlin • Heidelberg • New York ISBN 0-387-07628-X Springer-Verlag New York - Heidelberg • Berlin This work is subject to copyright. All rights are reserved, whether the whole or part of the materiaJ is concerned, specifically those of translation, re- printing, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under § 54 of the German Copyright Law where copies are made for other than private a use, fee is payable to the publisher, the amount of the fee to be determined by agreement with the publisher. © by Springer-Verlag Berlin • Heidelberg 1976 Printed in Germany Printing and binding: Beltz Offsetdruck, Hemsbach/Bergstr. TABLE OF CONTENTS Chapter 1 Introduction ................................... 1 Chapter 2 History and Literature Review .................. 5 2.1 Introduction ..................................... 5 2.2 Operational semantics ............................ 6 2.3 Denotational semantics ........................... i0 2.4 Propositional semantics .......................... 15 2.5 Complementary definitions ........................ 18 Chapter 3 Basic Elements of the Lattice-Theoretic Approach 22 3.1 Domains .......................................... 22 3.2 Functions ........................................ 24 3.3 Recursion ........................................ 27 Chapter 4 Complementary Definitions of a PASCAL Subset ... 30 4.1 Introduction ..................................... 30 4.2 An informal description of the PASCAL subset ..... 31 4.3 Abstract syntax of the PASCAL subset ............. 42 4.4 Mathematical semantics of the PASCAL subset ...... 44 4.5 Axiomatic semantics of the PASCAL subset ......... 61 Chapter 5 Consistency of the PASCAL Subset Definitions ... 77 5.1 Introduction ..................................... 77 5.2 The interpretation of assertions ................. 78 5.3 Substitution ..................................... 82 5.4 Interpretation of the axiomatic formulas ......... 84 5.5 Proof of consistency of the definitions .......... 86 5.6 Predicate transformers ........................... ii0 Chapter 6 Extensions to the PASCAL Subset Language ....... ll4 6.1 Introduction ..................................... 114 6.2 "Standard" semantics of the PASCAL subset ........ 115 6.3 The semantics of the extensions .................. 135 6.4 Type- and range-checking in PASCAL ............... 149 Chapter 7 Conclusions and Directions for Future Research .157 7.1 Conclusions ...................................... 157 7.2 Directions for future research ................... 159 Bibliography .............................................. 163 ABSTRACT This volume describes the use of mathematical and axiomatic semantics as a means of giving complementary definitions of the semantics of programming languages. We show that by giving descriptions of language semantics at different levels of abstraction, we can both: i. provide semantic definitions well-suited for the purposes for which formal descriptions are needed, e.g., proving properties of programs or showing implementations to be correct, and .2 develop a framework in which the issues involved in language design can be rigorously formulated. As an example of the use of complementary definitions, we present mathematical and axiomatic definitions of a large subset of PASCAL. Using the mathematical definition as a model for the more abstract axiomatic semantics, we show that the axioms and rules of inference are valid with respect to the mathematical model, i.e., the definitions are consistent. We also show that mathematical semantics provides a useful complement to axiomatic semantics because of .i the theory of computation underlying the mathematical approach, which provides important induction rules for proving the consistency of the~definitions, and 2. the ability to understand the difficulties involved in extending the axiomatic definitions in terms of the domain structure of the mathematical definition. The remainder of the monograph describes a number of possible extensions of the PASCAL subset in terms of their effect on the definitions given earlier. We show that certain constructs are inherently more complex than those used in the PASCAL subset, in terms of the domains necessary to give a simple, intuitive semantics of the constructs. ACKNOWLEDGEMENTS I would like to thank the following people for their assistance and encouragement during the production of this manuscript: Professor J.J. Horning, my thesis supervisor at the University of Toronto, Professor R.L. Constable, my external thesis examiner, Professors S.A. Cook, D.G. Corneil, and D.B. Wortman, the members of my thesis committee, and my wife, Marilyn, for all her patience and support. Also, the financial support of the Department of Computer Science, University of Toronto, and the National Research Council of Canada is gratefully acknowledged. And, the expert typing of Cheryl Stark and Debi Fields is greatly appreciated. CHAPTER 1 INTRODUCTION The literature of computer science is replete with ingenious advances in the use of programming languages to communicate to a computer more effectively the intent of the programmer. However, language designers find it far more difficult to find examples in the literature of useful meta-languages in which they can effectively communicate the intent of their programming language to the user. Natural languages have long been the principal medium of com- munication of programming language descriptions. Although such descriptions have strong appeal, particularly when they are as well- written as the Revised Algol Report [Naur 1963], there seem to be many instances when an informal description of the semantics of a programming language is inadequate for the needs of users, other designers, or implementors. The interest in the development and use of formal meta-languages to describe the semantics of programming languages is, in large measurer a reaction to the deficiencies of informal semantic descriptions. The goal of using formal methods to communicate understanding about programming languages has certainly not been the only motivation behind many of the efforts in formal semantics. The classical problems of program equivalence and implementation correctness also require formal semantic definitions. It is important to remember, however, that the primary goal of formal semantics is to provide more effective communication between the language designer and the various audiences with an interest in the language. One of the major problems in effectively communicating this intent is that we use the semantic description of a language at many different levels. At one level, a semantic definition should provide a means of reasoning about how to form programs using the facilities of the language, including the problems of guaranteeing the correctness of the programs produced. Semantic descriptions at a more detailed level are required as tools for language design and comparison. And, finally, sophisticated users and implementors may require language descriptions that give detailed descriptions of the sequence of operations invoked by each construct to judge the relative efficiency of programs written in the language or to have a useful implementation model. The complexities of programming languages also make the choice of an appropriate level of detail of a semantic description particularly important. For example, a compiler for a language provides a formal description of the semantics of the language. Yet the enormous amount of detail found in most compilers includes many notions irrelevant to an understanding of the language for many purposes, e.g., how to establish addressability on a particular machine. This detail only serves to cloud the essential character- istics of the language of interest to the casual user or language designer. Just as we can describe a program at several levels of abstraction, so it seems necessary to provide semantic descriptions at various "levels of abstraction" suited for the particular purpose for which a formal definition is required. This report develops the proposition, first made by Hoare and Lauer [1974], that these characteristics of the problem of semantic description of programming languages make any single definition technique unsuitable for giving the sole description of the semantics of the language. Instead, we propose giving semantic descriptions in terms of complementary definitions, i.e., a set of defintions, each defining the language at a particular level of abstraction, and each well-suited for use for particular purposes. We show that by using the axiomatic approach to semantics developed by Hoare [1969a, 1969b, 1971a] and the mathematical approach of Scott and Strachey [Scott 1970, Scott 1972c, Scott and Strachey 1972] as complementary definition techniques, it is possible to give complete descriptions of useful programming languages that are suitable for a variety of purposes. Although we could view the axiomatic definition as simply a useful abstraction of the mathematical definition, we will consider the definitions as truly complementary for two main reasons. First, as we will discuss further in the next chapter, the definitions given using each approach are definitely well-suited for different pruposes. Moreover, in Chapter ,4 we will use the implicit assumptions of the axiomatic approach to structure the domains used in the mathematical definition. Thus we not only use the mathematical definition to interpret the axiomatic definition, but we also use the axiomatic definition to impose limitations on the mathematical model. The monograph presents a mathematical and axiomatic treatment of a large subset of the programming language PASCAL [Wirth 1973a]. The major results include: i. Complete mathematical and axiomatic definitions of the PASCAL subset are given. The mathematical definition uses a domain structure which reflects the implicit assumptions of the axiomatic approach, and which is less powerful and less "machine-oriented" than the more common mathematical model used for similar languages, i.e., the so-called "standard" semantics [Ligler 1975a]. Additionally, the axiomatic definition includes a new treatment of the semantics of input and output. .2 The axioms and rules of inference given by the axiomatic definition are proven to be valid with respect to the model provided by the mathematical definition. We also suggest how the proofs given could be mechanically checked, or even generated, using an LCF-like [Milner 1972] formal logic. The use of mathematical semantics as a model of axiomatic definitions is similar to work recently done by George Ligler at Oxford [Ligler 1975a, 1975b]. .3 An interpretation of Dijkstra's "predicate transformers" [1973] is given and the properties of "healthy" predicate transformers are proven as theorems about the interpretat- ion. 4. The domain structure of mathematical definitions is used to analyze the limitations of the axiomatic approach and the "complexity" of certain language constructs. The organization of the volume is as follows. Chapter 2 provides a review of the literature and a history of the development of various approaches to semantics. Chapter 3 provides the basic elements of the lattice-theoretic approach to the theory of computation used in the remainder of the thesis to give the mathematical semantics of the PASCAL subset. Chapter 4 presents the definition of the PASCAL subset using the axiomatic and mathematical approaches. In Chapter 5 we give an interpretation of axiomatic formulas in terms of the model provided by the mathematical definition and present the proofs of consistency of the axiomatic definition and the mathematical definition of the PASCAL subset. Additionally, a Similar interpretat- ion of predicate transformers is presented. Chapter 6 discusses extensions to the language in terms of their effect on the semantic model used in the definitions~ Finally, we give summary, conclusions, and directions for future research in Chapter .7 CHAPTER 2 HISTORY AND LITERATURE REVIEW 2.1 Introduction The most obvious characteristic of the literature on the semantics of programming languages is its diversity of viewpoint. The purpose of this chapter is to organize some of the basic ideas present in semantics research and to give a developmental context for the work described in the thesis. The many different approaches to semantics can be roughly characterized as being of two different sorts: °i "Compiler-oriented." This form of semantics is exemplified by [Knuth 1968, Lee 1972, van Wijngaarden 1966]. In compiler-oriented semantic definitions, meaning is given in terms of a set of translations performed on some abstract representation of the syntactic structure (e.g., a parse tree) of programs in the language. 2. "Interpreter-oriented." In interpreter-oriented definitions, the meaning is given in terms of the "transformations" that may be specified by the syntactically valid programs in the language. The program text appears in the definitions more or less directly and transformations of the text are not included in the definition. All of the semantic models discussed in the remainder of this thesis will be interpreter-oriented models. Specifically, by an interpreter-oriented formal semantics of a programming language, we mean: .i a formal description of the "universe of discourse" for the language, i.e., the class of objects that may be manipulated by programs in the language. These objects could include "machine states," functions, normal form lambda expressions, assertions, or any other class of objects that may be formally specified. .2 a set of rules describing the ways in which the basic expressions in the language can be combined and giving the associated outcome ("value") of each of the combinations in