|
|
COMP2600: Formal Methods for Software Engineering
The 2011 Archive
Lecture Slides and Supporting Material
- Revision: Propositional Logic, Predicate Calculus
Week 1, Monday, July 25
Slides:
[pdf]
[pdf 2×2]
Find out about Aristotle
and Leibniz
- Revision: Sets, Functions, Relations, Induction
Week 1, Tuesday, July 26
Slides:
[pdf]
[pdf 2×2]
- Revision: Basic Haskell
Week 1, Thursday, July 28
Slides:
[pdf]
[pdf 2×2]
- Natural Deduction (Propositional Calculus)
Week 2, Monday, 1 August ; Tuesday 2 August (part)
Slides:
[pdf]
[pdf 2×2]
[Propositional Calculus Rules]
- Natural Deduction (Predicate Calculus)
Week 2, Tuesday 2 August (part), Thursday 4 August
Slides:
[pdf]
[pdf 2×2]
[Predicate Calculus Rules]
- Types and Recursion
Week 3, Monday 8 August
Slides:
[pdf]
[pdf 2×2]
Example code:
[Expression.hs]
[flatten.hs]
- Structural Induction
Week 3, Tuesday 9 August
Slides:
[pdf]
[pdf 2×2]
- Structural Induction (continued)
Week 3, Thursday 11 August
Slides:
[pdf]
[pdf 2×2]
- Specification with Z.
Week 4, Monday 14 August to Thursday 17 August
Slides:
[pdf]
[pdf 2×2]
New version with some errors fixed wentup at 18:30, Aug 18. See Forum.
You can download
The Z Reference Manual for free.
Jim Woodcock and Jim Davies also have a website for their book
Using Z
that you can browse on-line or download freely.
- Finite State Automata & Regular Languages
Week 5 Monday 22 August to Thurs 25 August
Slides:
[pdf]
[pdf 2×2]
- Language and Grammars
Week 6, Monday 29 August
Slides:
[pdf]
[pdf 2×2]
- Push-Down Automata
Week 6, Tuesday, 30 August
Slides:
[pdf]
[pdf 2×2]
- Introduction to Parsing
Week 6, Thursday, 1 September
Slides:
[pdf]
[pdf 2×2]
Example code:
[
ParseTypeDefs.hs]
[Expression Evaluator:
Main.hs
AbsSyn.hs
Scanner.hs
Parser.hs
Evaluator.hs]
- Lambda Calculus and Church Numerals
Week 7, Monday, 5 September
Slides:
[pdf]
[pdf 2×2]
[
Lambda Calculus Workbench]
[Mt. Lambda, near
Kyoto U.]
- Turing Machines
Week 7, Tuesday, 6 September
Slides:
[pdf]
[pdf 2×2]
- Complexity and Computability
Week 7, Thursday, 8 September
Slides:
[pdf]
[pdf 2×2]
- Hoare Logic - 3 lectures
Week 8, Monday (26 September), Tuesday (27 September)
and Thursday (28 September)
Slides:
[Monday, pdf]
[pdf 2×2],
[Tuesday, pdf]
[pdf 2×2],
[Thursday, pdf]
[pdf 2×2]
- Weakest Precondition Calculus - 3 lectures
Weeks 9 and 10, Tuesday (4 October), Thursday (6 October)
and Tuesday (11 October)
Slides:
[Tuesday, pdf]
[pdf 2×2],
[Thursday, pdf]
[pdf 2×2],
[Tuesday (week 10), pdf]
[pdf 2×2]
- Soundness and Completeness
Week 11, Monday, 17 October
Slides:
[pdf]
[pdf 2×2]
- Type Checking and Unification
Week 11, Tuesday 18 October
Slides:
[pdf]
[pdf 2×2]
- Prolog
Week 11, Thursday 20 October
Slides:
[pdf]
[pdf 2×2]
Example code:
[example files]
- Guest Lectures
Week 12, Tuesday (25 October) and Thursday (27 October)
Slides:
[Tuesday, pdf]
[pdf 2×2],
[Thursday, pdf]
[pdf 2×2]
|