Introduction to formal methods; predicate logic specification: foundations, methods of reasoning, axiomatic verification, formal specification with Z; algebraic specification: foundations, algebraic specification of ADTs, data type induction, verifying ADT implementations.