COMP2600: Formal Methods for Software Engineering

Lecture Material and Schedule

• Revision: Propositional Logic, Predicate Calculus
  Week 1, Monday
  Slides: [pdf] [pdf 2×2]
• Revision: Sets, Functions, Relations, Induction
  Week 1, Thursday
  Slides: [pdf] [pdf 2×2]
• No Lecture (Bush Week)
  Week 1, Friday
  
• Revision: Basic Haskell
  Week 2, Monday
  Slides: [pdf] [pdf 2×2]
• Natural Deduction
  Week 2, Wednesday
  Slides: [pdf] [pdf 2×2] [Propositional Calculus Rules]
• Natural Deduction (continued)
  Week 2, Friday
  Slides: [pdf] [pdf 2×2] [Predicate Calculus Rules]
• Soundness, Completeness and Consistency
  Week 3, Monday
  Slides: [pdf] [pdf 2×2]
• Types and Recursion
  Week 3, Thursday
  Slides: [pdf] [pdf 2×2]
  Example code: [Expression.hs]
• Structural Induction
  Week 3, Friday
  Slides: [pdf] [pdf 2×2]
• Structural Induction (continued)
  Week 4, Monday
  Slides: [pdf] [pdf 2×2]
• Hoare Logic
  Week 4, Thursday & Friday; Week 5, Monday
  Slides: [pdf] [pdf 2×2]
• Weakest Preconditions
  Week 5, Thursday & Friday; Week 6, Monday
  Slides: [pdf] [pdf 2×2]
• Lambda Calculus
  Week 6, Thursday
  Slides: [pdf] [pdf 2×2]
  [Lambda Calculus Workbench]
  [Mt. Lambda, near Kyoto U.]
• Church Encoding
  Week 6, Friday
  Slides: [pdf] [pdf 2×2]
• In-Class Practice Quiz
  Week 7, Monday
  During this class students may attempt a practice quiz to help gauge their progress. It is not for credit. The quiz will cover all material up to and including weakest preconditions. Ideally, you should come prepared with an A4 page of hand-written notes (both sides), as will be permitted in the final exam. The test should take about 1 hour to complete.
• Type Checking
  Week 7, Thursday
  (Back to the lambda calculus...)
  Slides: [pdf] [pdf 2×2]
• Finite State Automata & Regular Languages
  Week 7, Friday; continuing later
  Slides: [pdf] [pdf 2×2]
• Practice Quiz Discussion
  Week 8, Monday
  In this lecture we will work through some of the practice quiz questions. If you did not manage to complete the quiz during class, you should do so in your own time before this class.
  Here is Clem's attempt at the practice quiz.
• No Lecture
  Week 8, Thursday
  
• Finite State Automata & Regular Languages
  Week 8, Friday; Week 9, Monday
  Slides: [continued from week 7 - see above.]
• Language and Grammars
  Week 9, Thursday
  Slides: [pdf] [pdf 2×2]
• Push-Down Automata
  Week 9, Friday
  Slides: [pdf] [pdf 2×2]
• Introduction to Parsing
  Week 10, Monday
  Slides: [pdf] [pdf 2×2]
  Example code: [ParseTypeDefs.hs] [Expression Evaluator]
• Turing Machines
  Week 10, Thursday
  Slides: [pdf] [pdf 2×2]
  
• Complexity and Computability
  Week 10, Friday
  Slides: [pdf] [pdf 2×2]
  
• Course Review
  Week 12, Thursday and Friday
  [2008 Exam Paper] [ 2×1]