Assertions: a personal perspective

Assertions are Boolean formulas placed in program text at places where their evaluation will always be true. If the assertions are strong enough, they express everything that the programmers on either side of an interface need to know about the program on the other side, even before the code is written. Indeed, assertions can serve as the basis of a formal proof of the correctness of a complete program.