An assertion is a Boolean formula written in the text of a program, at a place where its evaluation will always be true — or at least, that is the intention of the programmer.
In the absence of jumps, it specifies the internal interface between the part of the program that comes before it and the part that comes after. The interface between a procedure declaration and its call is defined by assertions known as pre-conditions and post-conditions.
If the assertions are strong enough, they express everything that the programmers on either side of the interface need to know about the program on the other side, even before the code is written. Indeed, such strong assertions can serve as the basis of a formal proof of the correctness of a complete program.
The primary role of an assertion today is as a test oracle, defining the circumstances under which a program under test is considered to fail. A collection of aptly placed assertions is what permits a massive suite of test cases to be run overnight, in the absence of human intervention.
Failure of an assertion triggers a dump of the program state, to be analysed by the programmer on the following morning. Apart from merely indicating the fact of failure, the place where the first assertion fails is likely to give a good indication of where and why the program is going wrong.
And this indication is given in advance of any crash, so avoiding the risk that the necessary diagnostic information is over-written. So assertions have already found their major application, not to the proof of the correctness of programs, but to the diagnosis of their errors.
To read this external content, download the full paper. http://carlossicoli.free.fr/G/Gelenbe_E.,_Kahane_J.-P.-Fundamental_Concepts_in_Computer_Science_(Advances_in_Computer_Science_and_Engineering__Texts)-Impe.pdf#page=110