Formal Methods in Software Engineering COMP2600

Learning outcomes

More information may be available for enrolled students on the course website at http://cs.anu.edu.au/students/comp2600/

Upon completion of this course, the student will be able to do the following:

1. Apply the concepts of standard mathematical logic to produce proofs or refutations of well-formed propositions or arguments phrased in English or in a variety of formal notations (first order logic, discrete mathematics or Hoare Logic).
2. Given a description of a regular language, either in English, as a regular expression or as a grammar, generate a finite state automaton that recognizes that language. Similarly, given a deterministic or nondeterministic automaton, give a description of the language which it accepts.
3. Given an inductive definition of a simple data structure, write a recursive definition of a given simple operation on data of that type. Given some such recursively defined operations, prove simple properties of these functions using the appropriate structural induction principle.
4. Prove simple programs correct using Hoare Logic.
5. Prove correctness and termination of a simple program using the weakest precondition calculus.
6. Specify a simple system using Z.
7. Understand very simple Prolog programs.
8. Design a Turing Machine which will accomplish simple tasks.