---

INF2: Syntax and Semantics 2003

Lecture 12

---

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.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.
• Give a natural and a structural operational semantics for the looping construct from S₁ until b do S₂ Your rules should capture the following intuition about the behaviour of this construct:

  First the initialization statement S₁ is executed in the start state. The truth value of the boolean condition b is then checked in the state resulting from the execution of S₁. If b evaluates to true, then the execution terminates. Otherwise, the body S₂ of the loop is executed. The truth value of the boolean condition b is then checked in the state resulting from the execution of S₂. If b evaluates to true, then the execution terminates. Otherwise.....

  • Use your rules to evaluate from x:=0 until x = 2 do (y:= y - z;x:=x+1) from a state s where y has value 3 and z has value 1.
  • Can you find a statement in the language While that is equivalent to the construct from S₁ until b do S₂?