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).


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.
  • Venari project home page.