COMP2600: Formal Methods for Software Engineering - 2011

Assignments

There will be four assignments, with due dates probably Monday of weeks 6, 8, 10 and 12. Assignment specifications will be posted here as they are released.

Assignments are to be submited via the assignment boxes in the student foyer. All submissions must include a fully completed standard cover-sheet. If you do not include your tutor's name and your tutorial group, I have to spend time looking it up for you. You will be penalised at least 10%.

The assignments are normally marked out of 20.

• Assignment 1 - Natural Deduction and Structural Induction
  Due at 11am, Monday 29th August 2011
  Exercises
  Sample Solution
• Assignment 2 - Finite State Automata and Specification in Z
  Due at 11am, Monday 26th September 2011
  Exercises
  Z schemas are easy to typeset with the oz.sty package. It is described in ozguide.pdf
  Sample Solution


• Assignment 3 - Lambda Calculus, Grammars, PDAs and Turing Machines
  Due at 11am, Tuesday 11th October 2011
  Exercises
  File comb.hs referred to in the λ-calculus hint
  Sample Solution
  File solution.hs showing the λ-calculus β-reduction in Haskell


• Assignment 4 - Hoare Logic and Weakest Precondition Calculus
  Due at 11am, Monday 24th October 2011
  Exercises
  Sample Solution
  

Last year's assignments and sample solutions are available from the 2010 COMP2600 pages.