Protection from the Underspecified
Authors: Gary Leavens and Jeannette M. Wing
Submitted to Proceedings of 4th ACM SIGSOFT Symposium on the
Foundations of Software Engineering, 1995.
The full text of this paper is CMU-CS-96-129 (in
PostScript).
Abstract
Underspecification is a good way to deal with partial functions
in specification and reasoning.
However, when underspecification is used,
implementations may unintentionally be forced to depend
on parts of the specification that were supposed to be underspecified.
We show how to write pre- and postcondition specifications
that avoid such problems, by having the precondition ``protect''
the postcondition from the effects of underspecification.
This approach is most practical if the specification of mathematical vocabulary
is separated from the specification of implementation behavior, as in Larch,
because it gives the specifier a chance to think about protection
separately from the specification of mathematical behavior.
We formalize the notion of protective procedure specifications,
and show how to prove that a specification is protective.
We also extend the Larch Shared Language
to allow specification of what is intentionally left underspecified,
which also allows enhanced ``debugging'' of such specifications.