ENGINEERING 9880

TITLE: Special Topics in Computer Engineering: Program Specificaton and Calculation.

RATIONAL: This course is intended as an introduction to formal methods of programming and software engineering. It is intended to give engineering students (from any area) and computer science students an understanding of mathematical approaches to software construction and to give students intending to specialize in formal aspects of software engineering a firm grounding for self study and research. As a prerequisite, students should be able to program in a high level programming language and have some exposure to propositional logic.

FORMAT: Lectures.

COURSE OUTLINE:

• Review of propositional logic, discrete mathematical structures, and predicate logic.
• Program specification.
• Formal documentation.
• Laws of program derivation.
• Strategies for developing loops and recursive procedures.
• Data refinement and module design.
• Abstract algorithm development.
• Parallel, communicating, and nonterminating processes.
• Hardware verification.
• Time permitting: Use of theorem provers, Proof by annotation. Survey of other formalisms.

TEXT:

• Eric C. R. Hehner, A Practical Theory of Programming, Springer-Verlag, 1993.
• Theodore Norvell, Supplemental notes for 9880.

REFERENCE:

• Carroll Morgan, Programming from Specifications, Prentice Hall International, 1994.
• David L. Parnas et al, papers on formal documentation of programs.

• About this document ...