The author of this volume sets out to show how it is possible to give complete and unambiguous definitions of the meaning of every feature of modern programming languages and how formal versions of such definitions may serve as a basis for making compilers and interpreters for the languages. It also explains how to give students a training in the use of formal methods. There are several methods for defining the semantics of programming languages. In this book, the author focuses mainly on the denotational method, although operational and proof theoretical semantics are treated as well. It shows how to define the semantics of imperative languages, whilst the functional language, ML, is used to implement the formal definitions. The book also covers objects and classes, which provides formal definitions of the semantics of the main features of object-oriented languages.
Table of Contents:
A very simple language; concrete syntax; concrete and abstract syntax; informal, operational semantics; formal, denotational semantics; implementing Loop in ML; abstract syntax of loop in ML; semantics of loop in ML; an interpreter of abstract loop programs; parsing loop; algebras; basic algebras; compound algebras constructing algebras; modular, algebraic semantics; compositionality; fixpoint theory; undefined operations and infinite loops; recursively defined mappings; complete partial orders; continuous functions; strict extensions of functions; fixpoints; a Language with errors and infinite loops; a richer language; syntax of While; standard semantics of While; semantic equivalence; the While theorem; While in ML; operational semantics; proof theoretical semantics; formal deductive calculi; natural semantics; axiomatic semantics; declarations of data structures; a language with variables and constants; untyped semantics of Decl0; layered semantics of Decl0; Decl0 in ML; typed semantics of Decl0; Decl1 - A language with arrays; procedures and functions; a taxonomy of parameter transmissions; var, val and value parameters; name parameters; lazy parameters; floating procedures and functions; objects and classes; syntax and informal semantics; semantic domains; semantic mappings; subclasses and inheritance; continuations and jumps; exits and stops; layered continuation semantics; Goto's; expressions that change the state; exceptions; nondeterminism and concurrency; nondeterminism; powerdomains; concurrency; reflexive domains; domain equations; sets of non-negative integers; the Lambda language; using Lambda; retracts; how to solve domain equations.