@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(Protection from the Underspecified)
@heading(CMU-CS-96-129)
@center(@b(Gary T. Leavens@foot<Department of Comuter Science, Iowa State University, Ames, Iowa 50011>, Jeannette M. Wing))
@center(April 1996@foot<Submitted to the ACM SIGSOFT Symposium on Foundations of Software Engineering 1996.>)
@center(FTP: CMU-CS-96-129.ps)
@blankspace(1)
@begin(text)

Underspecification is a good way to deal with partial functions in
specification and reasoning.  However, when underspecification is used,
implementations may unintentially 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 more 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 spearately 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.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Partial and total functions; protective specifications;
specification languages, underspecification; Larch>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(24 pages)])