Protection from the Underspecified

Leavens, Gary T. and Wing, Jeannette M. (1996) Protection from the Underspecified. Technical Report TR96-04, Department of Computer Science, Iowa State University.

Abstract

Protection from the Underspecified
by
Gary T. Leavens and Jeannette M. Wing
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.


Subjects:
All uncategorized technical reports


ID code:
00000125
Deposited by:
Staff Account on 29 April 1996





Contact site administrator at: ssg@cs.iastate.edu