. . . so the postcondition becomes true at the function’s end.

• The programmer who writes the function counts on the precondition being valid, and ensures that the postcondition becomes true at the function’s end.

Previous slide

Next slide

Back to first slide

View graphic version