COMP2600: Formal Methods for Software Engineering - 2012

Assignments

There will be four assignments, due mid-morning on the Mondays 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 and you too will be penalised.

The assignments are normally marked out of 20.

• Assignment 1 - Natural Deduction and Structural Induction
  Due at 11am, Monday 27th August, 2012
  Exercises
  Example LaTeX Sources: LatexSolution.tex (main file), fitch.sty, mya4.sty
  Sample Solution


• Assignment 2 - Hoare Logic and Weakest Precondition Calculus
  Due at 11am, Monday 24th September, 2012
  Exercises
  Sample Solution
  


• Assignment 3 - System Specification in Z, Lambda Calculus and Prolog
  Due at 5pm, Thursday 11th October, 2012  ** NOTE NEW DEADLINE **
  Exercises. (Updated to reflect deadline change and fixed DFA/NFA typo (as announced).)
  Z schemas are easy to typeset with the oz.sty package. It is described in ozguide.pdf
  Sample Solution


• Assignment 4 - Finite State Machines and Grammars
  Due at 11am, Wednesday 24th October 2012  ** NOTE NEW DEADLINE **
  Exercises
  Example LaTeX sources: sample_automata.tex (sample automata), automata.tex (macros)
  Sample Solution
  

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