Formal verification: loop invariants, fixpoint induction;
also, the `cut-and-paste' principle.
Type conversion, unsigned types, sign extension.
C string library.
Pointers, Malloc() and Calloc()
This module will be examined in a 2 hour exam in Trinity term.
20% of the final mark will be based on course work,
(10% programming assignments, including a formal programming test & 10% quizzes) and the other 80% on the exam. Re-assessments if required will consist of 100% exam.