Next / Previous / Shipman's Home Sweet Homepage / Site map

Cleanroom intended functions: Preconditions

The intended functions discussed previously (see compound intended functions) describe what a procedure does in every case. However, it is not always possible or necessary to define what a function does for all possible inputs.

You can write a precondition on an intended function without specifying what happens if that precondition is not met:

    # [ if precondition ->
    #	  intended-function-1 ]
For I/Fs of this form, the behavior of that procedure is not defined in the cases where the given precondition is false.

This shifts the burden of supplying the precondition onto the caller. If another module calls such a procedure, but it cannot guarantee that the precondition is met, the caller's code cannot be verified.

Next: Cleanroom intended functions: Partial specification
See also: Writing Cleanroom intended functions
Previous: Cleanroom intended functions: Compound I/Fs
Site map
John W. Shipman,
Last updated: 2002/09/28 01:14:33