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.