![[I2 logo]](../../../../Images/i2.gif)
![[RWTH logo]](../../../../Images/rwth-rot90.gif)
|
MOVES: Software Modeling and Verification
(Informatik 2)
|
Semantics of Programming Languages
Fall 2002/03
Diplomstudiengang Informatik,
Masterstudiengang Software Systems Engineering
(Theoretical CS, Specialization Subject)
News
- 17.10.2002
-
Change of locations:
-
Because of the bad lighting at AH IV, the lecture is moved
to the room 6019 (in the ground floor of the E2 part of the
CS building), starting Oct. 24.
-
Due to special reservations, the tutorial has to take place
in AH VI (rather than AH III) on Nov. 6, 2002.
Dates
| Kind |
Time |
Place |
Start |
Docent |
| Lecture |
Thu 10:00-11:30 |
6019 |
17.10. |
Noll |
| Exercises |
Wed 14:00-15:30 |
AH III (06.11.02: AH VI)
|
23.10. |
Noll |
Contents
Studying the imperative model language WHILE, the most prominent methods
for specifying the formal semantics of programming languages are being
introduced:
-
The denotational semantics, which defines the input/output
relation of a program by means of structural induction,
-
The operational semantics, which describes the execution
behaviour of a program, and
-
The axiomatic semantics, which supports the proof of
program properties.
Slides
- Introduction (in German)
- Syntax of WHILE
- Operational Semantics of WHILE (no slides)
- Denotational Semantics of WHILE
-
Equivalence of Operational and Denotational Semantics (no slides)
- Axiomatic Semantics of WHILE
-
Extension of WHILE by Blocks and
Procedures
Excursus: Proof by Structural Induction
Exercises
| No. |
Issued |
Due |
Presentation (where) |
Sheet |
| 1 |
24.10.02 |
31.10.02 |
06.11.02 (AH VI) |
here |
| 2 |
07.11.02 |
14.11.02 |
20.11.02 (AH III) |
here |
| 3 |
21.11.02 |
28.11.02 |
04.12.02 (AH III) |
here |
| 4 |
05.12.02 |
12.12.02 |
18.12.02 (AH III) |
here |
| 5 |
09.01.03 |
16.01.03 |
22.01.03 (AH III) |
here |
| 6 |
23.01.03 |
30.01.03 |
12.02.03 (AH III) |
here |
Literature
|
![[Mail]](../../../../Images/umschlag.gif)
Home
