---

INF2: Syntax and Semantics 2003

Lecture 10

---

Topics

In this lecture, we begin our semantic analysis of While by offering two operational semantics for its statements. We shall describe a natural and a structural operational semantics for While, and discuss what these two (equivalent, but different) semantics tell us about the behaviour of statements.

Should you be interested in seeing how easy it is to implement natural and structural operational semantics for our example language, you may wish to look at the Miranda implementations of evaluation of expressions, and of the natural and structural operational semantics. (Courtesy of Hanne Riis Nielson and Flemming Nielson.)

Time and Location

Reading Material

• Reading Material: Sections 2.1 and 2.2 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.3(*), 2.4, 2.7(*) in Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction. Wiley Professional Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.

• (*) Dr. X has recently developed the following programming language, which he calls XL. The syntax of the language is the following:
  P ::= ass(x,a) | P1 poi P2 | cond(Z(x),P1,P2) | fai P fino Z(x)

  where x ranges over variables, and a over arithmetic expressions as in the language While. Dr. X has provided the following semantics for XL, using the natural semantics approach:

  (ass(x,a),s) ---> s[x |--> v] if v is the value of a in state s

  (P1,s) ---> s', (P2,s') ---> s''
  --------------------------
  (P1 poi P2,s) ---> s''
  

  (P2,s) ---> s'
  ---------------------- if s(x)=0
  (cond(Z(x),P1,P2),s) ---> s'
  

  (P1,s) ---> s'
  --------------------- if s(x) > 0
  (cond(Z(x),P1,P2),s) ---> s'
  

  (P,s) ---> s'
  ------------------- if s'(x) = 0
  (fai P fino Z(x),s) ---> s'
  

  (P,s) ---> s' (fai P fino Z(x),s') ---> s''
  --------------------------------- if s'(x) > 0
  (fai P fino Z(x),s) ---> s''
  

  Write a program in XL that, when started in a state s, computes the factorial of the value of s(x) and assigns it to a variable y. Using the above rules, check that your program does what it should do when it is run from a state in which x has value 3.