Date Added: Aug 2011
This paper gives a quick tutorial introduction to functional program verification. In functional program verification, a program is viewed as a mathematical function from one program state to another, and proving its correctness is essentially comparing two mathematical functions, the function computed by the program and the specification of the program. The reader is assumed to have some programming experience and to be familiar with sets and functions. Software is used widely in almost every aspect of the authors' daily lives. Even the smallest devices such as cellular phones and PDAs are controlled by software. Software contains defects.