Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Syntax and Semantics
In lecture 9, we introduced
two operational semantics for the language While, viz. a
natural and a structural operational semantics. Both
semantics were defined using a collection of syntax directed rules
that allow us to deduce the behaviour of a composite program from that
of its constitute 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
Tuesday, 7 December 2004 at 9:00 in room 303.
Reading Material
Primary Reading: Pages 26-32 and 36-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
If you have not already done so, work out some of the
exercises on Structural Operational Semantics for While
mentioned on the web page for lecture 9. I
recommend that you attempt exercise 2.17(*). Exercise 2.18 is for the
keenest.
Exercises 2.11(*), 2.13, 2.21(*), 2.22(*), 2.24 in Hanne Riis Nielson, Flemming Nielson: Semantics with
Applications: A Formal Introduction. Wiley Professional
Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.
For the Keenest: Exercise 2.10 in Hanne Riis Nielson, Flemming Nielson: Semantics with
Applications: A Formal Introduction. Wiley Professional
Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.