Post Condition

Pre-conditions and post-conditions are used in formal specification to specify an operation, which is essentially a state change. Typically, any conditions not specifically stated as post-conditions are not constrained. For example, a deletion operation in which element n is deleted from set S has a post-condition that n is not in S. To work properly, it also needs a post-condition that says that all other elements of S before the deletion, except for n are still in S afterward. When describing operations in terms of pre-conditions and post-conditions, you are stating only the essential what, carefully avoiding the how. Note the close relationship between specifications and tests.

Here is a testing strategy: use post conditions like UnitTests. Inside the method when it is done with the work it has to do it tests its result to see if it is as expected. This checking can be much more specific than an Assertion. As a simple example if the method computes sqrt(x), the post condition can test if result*result==x.

assert(result * result == x);

Good idea, bad example. Think RoundingError?.

The main advantage here is that the state information is fresh and easily accessible inside the method. Some of this will be lost when the UnitTest gets around to examining the outcome.

There is a cost in execution speed. If this is significant then use macros to conditionally compile these post conditions. Or leave them in (ShipWithAssertionsOn) and have a live monitoring system constantly test your code as it runs. The post conditions could log errors and be otherwise non-obtrusive (ReportBugsSilently).

Here is an example: a database is updated and then tested to see if the updated record has the correct values. It is easier to describe a thing than it is to construct it. And so this testing of correctness is easier than the computation. -- AsimJalis.

The downside is that all of the post conditions can greatly inflate the code, making it harder to read. which is why it is best to associate the contracts with interfaces, not the implementation.