COSC 3111.03 Introduction to Program Verification
Section M Winter Mon, Wed 11:30-13:00
Every program implicitly asserts a theorem to the effect that if certain
input conditions are met then the program will do what its specifications
or documentation says it will. Making that theorem true is not merely a
matter of luck or patient debugging; making a correct program can be greatly
aided by a logical analysis of what it is supposed to do, and for small
pieces of code a proof that the code works can be produced hand-in-hand
with the construction of the code itself. Good programming style works
in part because it makes the verification process easier and this in turn
makes it easier to develop more complex algorithms from simple ones.
The course will provide an introduction to the basic concepts of formal
verification methods. It will also including the use of simple tools to
aid in verification.
Topics covered may include the following.
- The role of formal verification in the software life- cycle; verification
vs. testing and validation
- Introduction to propositional calculus; checking for tautologies and
contradictions; annotating code with assertions
- Moving from goals to starting points; proving relative correctness
for small code segments
- Creating specifications with quantifiers; translating specifications
into loops; establishing termination
- Possibilities for the automatic synthesis of programs from specifications.
Texts: Gries, D., The Science of Programming, Springer-Verlag:
- A Logical Approach to Discrete Math. Gries and Schneider. Springer-Verlag.
- Backhouse, R., Program Construction and Verification, Prentice-Hall:
prerequisites, including MATH2090.03