Assertions in Programming: From Scientific Theory to Engineering Practice

Abstract

An assertion in a computer program is a logical formula (Boolean expression) which the programmer expects to evaluate to true on every occasion that program control reaches the point at which it is written. Assertions can be used to specify the purpose of a program, and to define the interfaces between its major components. An early proponent of assertions was Alan Turing (1948), who suggested their use in establishing the correctness of large routines. In 1967, Bob Floyd revived the idea as the basis of a verifying compiler that would automatically prove the correctness of the programs that it compiled. After reading his paper, I became a member of a small research school devoted to exploring the idea as a theoretical foundation for a top-down design methodology of program development. I did not expect the research to influence industrial practice until after my retirement from academic life, thirty years ahead. And so it has been.

In this talk, I will describe some of the ways in which assertions are now used in Microsoft programming practice. Mostly they are used as test oracles, to detect the effects of a program error as close as possible to its origin. But they are beginning to be exploited also by program analysis tools and even by compilers for optimisation of code. One purpose that they are never actually used for is to prove the correctness of programs. This story is presented as a case study of the way in which scientific research into ideals of accuracy and correctness can find unexpected application in the essentially softer and more approximative tasks of engineering.