9 WRITE PRE- AND POST-CONDITIONS FOR METHOD POP.NOTE THAT TRUTH OF...

17.9

Write pre- and post-conditions for method

pop

.

Note that truth of assertions does not guarantee that the software is working cor-

rectly. However, if the value of an assertion is false, then there certainly is a fault in the

software. Note also that violation of a precondition means that there is a fault in the

user of the method; a violation of a postcondition means a fault in the method itself.

There are two main ways to make use of assertions. One way is to write assertions as

comments in a program, to assist in manual verification. On the other hand, as indicated

by the notation used above, some programming languages (including Java) allow asser-

tions to be written as part of the language – and their correctness is checked at run-

time. If an assertion is found to be false, an exception is thrown.

There is something of an argument about whether assertions should be used only

during development, or whether they should also be enabled when the software is put

into productive use.