Example

// Precondition: x >= 0.

// Postcondition: The square root of x has

// been written to the standard output.

...

}

The postcondition always indicates what work the function has accomplished. In this case, when the function returns the square root of x has been written.

The postcondition always indicates what work the function has accomplished. In this case, when the function returns the square root of x has been written.