Comp 317 is a third-year option that runs in the second semester, and is taught by Grant Malcolm.
Office hours are Mondays, 15:00-16:00, Room 2.19, Ashton Building
The recommended text for this course is
Algebraic Semantics of Imperative Programs
by Joseph A. Goguen and Grant Malcolm,
MIT Press, 1996.
Find it
in the library
The lectures will be based mainly on this text, but there are
several topics in this course not covered there;
hand-outs will be given as appropriate.
The Continuous-Assessment component of the module consists of a class test, lasting 45 minutes and counting for 10% of the final grade, and one practical assignment, also counting for 10% of the final grade. There will also be a two-hour written exam counting for the remaining 80% of the final grade. A date for the class test will be arranged during lectures, and example questions will be made available beforehand.
Previous final exams (PDF files):
You should make your own notes during the lectures; some background material will be made available here as the course progresses.
An outline of the syllabus is:
Lecture 1. Introduction to the module.
Hand-outs: Introduction;
Chapter 1 of Tennent, Semantics. Prentice-Hall, 1991.
Lecture 2. The module in a nutshell:
syntax and semantics of binary numerals.
Hand-out: Problem Sheet 1
Solutions
Lecture 3. The syntax and semantics of SIMPLE:
expressions.
Hand-out: Denotational Semantics
Lecture 4. The semantics of SIMPLE: assignments.
Lecture 5. The semantics of SIMPLE:
sequential composition and conditionals.
Hand-out: Problem Sheet 2
Solutions
Lecture 6. The semantics of SIMPLE: while-loops.
Lecture 7. Extending the syntax and semantics of SIMPLE.
Hand-out: 2009-10 exam paper
Lecture 8. Extending the syntax and semantics of SIMPLE.
Hand-out: Problem Sheet 3
Solutions
Lecture 9. Maude.
Lecture 10. Maude: Modules, Signatures and Models
Lecture 11. Maude:
Models: the Term Algebra
Hand-outs:
Lecture 12. Maude:
Subsorts and Syntax of SIMPLE.
Hand-outs:
Lecture 13. Maude: Equations.
Lecture 14. Maude:
Term-rewriting.
Hand-out: Problem Sheet 5 (PDF)
Solutions (PDF)
Lecture 15. Term-rewriting.
Hand-out: Practical Assignment (PDF)
Lecture 16. Models: satisfaction of equations.
Lecture 17. Initial algebras of equational theories.
Hand-out: Problem Sheet 6 (PDF)
Solutions (PDF)
Lecture 18. Semantics of SIMPLE in Maude: expressions.
Hand-outs:
Lecture 19. Semantics of SIMPLE
Lecture 20. Semantics of SIMPLE: while-loops
Hand-out: notes on Program Verification
Hand-out: Problem Sheet 7 (PDF)
Solutions (PDF)
Hand-out: The Rewriting Logic Semantics Project (PDF)
See also the Maude session
from the lecture.
Lecture 21. Correctness of Programs: specification
Lecture 22. Conditionals and case-analysis.
Lecture 23. Invariants of loops.
Problems for next tutorials:
all exercises from
notes on Program Verification.
Solutions
Lecture 24. More invariants.
Lecture 25. More invariants.
Handout - solutions to the first assignment:
exceptions.maude.
exceptionSemantics.maude.
Lecture 26. Semantics of Data Structures: arrays.
Handout:
Problem Sheet 9.
Lecture 27. Semantics of Data Structures: arrays.
Hand-out: 2nd practical assignment (PDF)
Revision Lectures. Question 5 will be a "general semantics"
question; see Questions 5 and 6 in the hand-out.
Hand-out: