---

INF2: Syntax and Semantics 2003

Lecture 11

---

Topics

Both natural and structural operational semantics are defined using a collection of syntax directed rules that allow us to deduce the behaviour of a composite program from that of its component subprograms. This type of semantic description has been pioneered by Gordon Plotkin, and is widely used in the semantics of programming and specification languages. For this reason, we shall spend some time on the analysis of the general form of these two semantics, and on pinpointing the proof techniques that they naturally support. To highlight the use of these proof techniques, we shall see how using operational semantics we can formally argue about equivalence, and about desired properties of a programming language, e.g., that its programs are deterministic. A program is deterministic if the final result of its execution (if one exists) is completely determined by the initial state.

Time and Location

Reading Material

• Primary Reading: Pages 32-44 of Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction. Wiley Professional Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992. (postscript)

Exercises

• Exercises 2.16(*), 2.17(*), 2.18 (for the keenest), 2.22 and 2.23(*) in Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction. Wiley Professional Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.