Supplementary Description: P515 combines introductions to three areas:
formal logic, specification and verification of imperative programs,
and specification of system behaviour.
Students registered to the course under the P415 listing would be
dispensed of some of the more challenging projects and exam questions,
but otherwise the course will be run at the graduate level.
