Assertions in programming: From scientific theory to engineering practice: Keynote address

Abstract

An assertion in a computer program is a logical formula (Booleanexpression) which the programmer expects to evaluate to true on every occasionthat program control reaches the point at which it is written. Assertions can beused to specify the purpose of a program, and to define the interfaces betweenits 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 thatwould automatically prove the correctness of the programs that it compiled.After reading his paper, I became a member of a small research school devotedto exploring the idea as a theoretical foundation for a top-down designmethodology of program development. I did not expect the research toinfluence industrial practice until after my retirement from academic life, thirtyyears ahead. And so it has been.In this talk, I will describe some of the ways in which assertions are nowused in Microsoft programming practice. Mostly they are used as test oracles, todetect the effects of a program error as close as possible to its origin. But theyare beginning to be exploited also by program analysis tools and even bycompilers for optimisation of code. One purpose that they are never actuallyused for is to prove the correctness of programs. This story is presented as acase study of the way in which scientific research into ideals of accuracy andcorrectness can find unexpected application in the essentially softer and moreapproximative tasks of engineering.