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.

Examination and Class Work

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):

• 2009-10
• 2008-09
• 2007-08
• 2006-07
• 2005-06
• 2004-05
• 2003-04

Lecture Notes

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:

• Introduction
• Denotational Semantics
• Semantics of Data Structures and Axiomatic Semantics (under construction) (also, some supplementary notes on OBJ, also under construction)
• Program Verification
• Further Data Types

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

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

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

Lecture 9. Maude.

Lecture 10. Maude: Modules, Signatures and Models

Lecture 11. Maude: Models: the Term Algebra
Hand-outs:

• Problem Sheet 4 (PDF)
• About the Class Test

Lecture 12. Maude: Subsorts and Syntax of SIMPLE.
Hand-outs:

• Syntax of SIMPLE

Lecture 13. Maude: Equations.

Lecture 14. Maude: Term-rewriting.
Hand-out: Problem Sheet 5 (PDF)

Lecture 15. Class Test.

Lecture 16. Models: satisfaction of equations.

Lecture 17. Initial algebras of equational theories.
Hand-out: Problem Sheet 6 (PDF)

Lecture 18. Semantics of SIMPLE in Maude: expressions.
Hand-outs:

• Semantics of SIMPLE

Lecture 19. Semantics of SIMPLE

Lecture 20. Semantics of SIMPLE: while-loops
Hand-out: notes on Program Verification
Hand-out: Problem Sheet 7 (PDF)

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.

Lecture 24. More invariants.

Lecture 25. More invariants.

Lecture 26. Semantics of Data Structures: arrays.
Handout: Problem Sheet 9.

Lecture 27. Semantics of Data Structures: arrays.

On-line Resources

• Maude:
  • The Maude homepage has downloads for Linux, Macs, Windows; documentation, etc.
  • Moment also provides a download for Windows that doesn't require Cygwin.
  
   
• A tutorial on BNF by Lars Marius Garshol.
   
• The Algol60 Report, which has a useful introduction to BNF.
   
• A tutorial introduction to denotational semantics by R.D. Tennent, "The denotational semantics of programming languages", Communications of the ACM, 19(8):437-453, 1976. (PDF)