P515 combines introductions to three areas:
formal logic, specification and verification of imperative programs,
and specification of system behavior. 

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.  

The course is being redesigned, and the following outline is tentative.

    I Data
        I.1 Sets
        I.2 Inductive processes 

    II. Structures
        II.1 Term structures
        II.2 General structures
        II.3 Formal descriptions
        II.4 The axiomatic method 

    III. Program verification and development: Part 1.
        III.1 Imperative programs
        III.2 Program annotation
        III.3 Program development 

    IV. Formal proofs
        IV.1 Propositional logic
        IV.2 First order proofs
        IV.3 Completeness 

    V. System specification
        V.1 The TLA Specification Language
        V.2 Temporal logic
        V.3 Temporal specifications in TLA 

    VI. Program verification and development: Part 2 (if time allows)
        VI.1 Recursive procedures
        VI.2 Semantics of recursive programs
        VI.3 Proving and developing recursive programs