HP Integrity NonStop J-Series - Manual (Page 257)

The case just described would trigger a failure because operator[]would find that the
PRECONDITION is not met.
Here's a slightly more complicated example:
template void List::insert(T* obj){
RWPRECONDITION( obj!= 0 );
head = new Link(head, obj);
RWPOSTCONDITION( this->contains(obj) );
}
In this example, the job of the function insert() is to insert the object pointed to by the argument
into a linked list of pointers to objects of type T. The only precondition for the function to work
is that the pointer obj not be null. If this condition is satisfied, then the function guarantees to
successfully insert the object. The condition is checked by the postcondition clause.
The macros RWPRECONDITION and RWPOSTCONDITION are defined in and
compile out to no-ops, so long as the preprocessor macro RWDEBUG is not defined. Here's
what appears in the makefile:
#ifdef RWDEBUG
# define RWPRECONDITION(a) assert(a)
# define RWPOSTCONDITION(a) assert(a)
#else
# define RWPRECONDITION(a) ((void*)0)
# define RWPOSTCONDITION(a) ((void*)0)
#endif