Example

void write_sqrt( double x)

// Precondition: x >= 0.

// Postcondition: The square root of x has

// been written to the standard output.

...

}

• In this example, the precondition requires that

x >= 0

be true whenever the function is called.

Previous slide

Next slide

Back to first slide

View graphic version