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 the previous three lectures, 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
Thursday, 27 March 2003 at 10:15 in A4-106.
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)
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.
Consider the construct
S1if-abort-then S2 .
The idea is that S1if-abort-then S2 runs
like S1, but if the computation of S1 aborts,
then S2 is executed from the state in which S1
aborted.
Would you you use natural or structural operational semantics to
describe the operational semantics of this construct? Why?
Give rule(s) defining the semantics of your choice.