Book excerpts:

This book is developed out from the experiences of teaching courses covering the formal semantics of programming languages. Although the specification methods are formal, the presentation is "gentle", providing just enough in the way of mathematical underpinnings to produce an understanding of the metalanguages. Enough coverage of mathematics and formal methods are presented to justify the definitional techniques, but the text is accessible to students with a basic grounding in discrete mathematics as presented to undergraduate computer science students.

There has been a tendency in the area of formal semantics to create cryptic, overly concise semantic definitions that intimidate students new to the study of programming languages. The emphasis in this text is on clear notational conventions with the foremost goals of readability and understandability.

Along the way, laboratory exercises were developed in implementing small programming languages in Prolog following denotational definitions. Prolog proved to be an excellent tool for illustrating the formal semantics of programming languages. It turned out that these laboratory exercises were highly successful in motivating students since the hands-on experience helped demystify the study of formal semantics. Although this text has been carefully written so that the laboratory activities can be omitted without loss of continuity, most readers should try the laboratory approach and experience the same success observed in the author's classes.

As with other textbooks in this field, this books also introduces the basic concepts using mini-languages that are rich enough to illustrate the fundamental concepts, yet sparse enough to avoid being overwhelming.

Wren, a simple imperative language with two types, integer and Boolean, thus allowing for context-sensitive type and declaration checking. It has assignment, if, while, and input/output commands.

Pelican, a block-structured, imperative language, is an extension of Wren containing the declaration of constants, anonymous blocks, procedures, and recursive definitions.

The description of continuations in denotational semantics requires a modified version of Wren with goto statements, called Gull. This minilanguage can be skipped without loss of continuity if continuations are not covered.