A verifying compiler is one that proves automatically that a program is correct before allowing it to be run. Correctness of a program is defined by placing assertions at strategic points in the program text, particularly at the interfaces between its components. From recent enquiries among software developers at Microsoft, I have discovered that assertions are widely used in program development practice. Their main role is as test oracles, to detect programming errors as close as possible to their place of occurrence. Further progress in reliable software engineering is supported by programmer productivity tools that exploit assertions of various kinds in various ways at all stages in program development. The construction and exploitation of a fully verifying compiler remains as a long-term challenge for twenty-first century Computing Science. The results of this research will be of intermediate benefit long before the eventual ideal is reached.


Program Correctness Java Modelling Language Program Text Test Oracle Academic Ideal 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Tony Hoare
    • 1
  1. 1.Microsoft Research Ltd.CambridgeUK

Personalised recommendations