The verification of software and hardware is, in general, an extremely complex task, one that is almost impossible to carry out fully in most cases. Even so, it is highly desirable that during the writing of programs efforts be made to ensure that the code written is provably correct. The challenge is to write code in a manner that allows for an easy proof of correctness. Such a proof should clarify the nature and working of the program and should serve as a demonstration that the program achieves the end for which it was written. In many cases, a full and formal proof of correctness is never made, but the concepts involved in finding such a proof nevertheless have profoundly influenced good programming practice.

In order to understand the general nature of correctness analyses, some basic terms must be defined. A block is a section of code with...