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. These two semantics are equivalent for this basic
language (cf. Theorem 2.26 in Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal
Introduction. Wiley Professional Computing, (240 pages, ISBN 0
471 92980 8), Wiley, 1992).
In this lecture, we shall see how to describe the operational
semantics of common constructs in many high-level programming
languages. More precisely, we shall examine extensions of the basic
language While with features like for-loops, abortion,
nondeterminism and parallelism. Our aim in examining these extensions
of While will be twofold:
First, we shall gain insight on the wide applicability of
operational semantics to give the formal semantics to programming
languages.
Second, we shall discuss what type of semantics is good for
what purposes.
We shall see that natural and structural operational semantics do not
apply equally well to all of these extensions of While.
Time and Location
Wednesday, 8 December, 2004 at 9:00 in room 303.
Reading Material
Primary Reading: Section 2.4 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)
Supplementary Optional Reading on Semantics for Guarded
Commands and a Subset of Occam: Chapter 6 of The Semantics of
Programming Languages: An Elementary Introduction Using Structural
Operational Semantics by Matthew
Hennessy. (Available for photocopying from me.)
Exercises
Exercises 2.32(*), 2.33, 2.34(*), 2.35(*), 2.36 in Hanne Riis Nielson, Flemming Nielson: Semantics with
Applications: A Formal Introduction. Wiley Professional
Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.
(*) Answer questions (i) and (iii) in part 1 of this semantics
written exam from Aarhus. [Note: In that file,
IMP is just our language While.]