archives

Protection from the Underspecified


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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

Full text available as:Postscript
Adobe PDF

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