@device(postscript) @libraryfile(Mathematics10) @libraryfile(Accents) @style(fontfamily=timesroman,fontscale=11) @pagefooting(immediate, left "@c", center "@c", right "@c") @heading(Protective Interface Specifications) @heading(CMU-CS-96-129R) @center(@b(Gary T. Leavens@foot, Jeannette M. Wing)) @center(April 1996, Revised October 1996@foot) @center(FTP: CMU-CS-96-129R.ps, CMU-CS-96-129Rcover.ps) @blankspace(1) @begin(text) The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these functions are partial, or underspecified, then the procedure specification may not be well-defined. We show how to write pre- and postcondition specifications that avoid such problems by having the precondition "protect" the postcondition from the effects of partiality and underspecification. We formalize the notion of protection from partiality in the context of specification languages, and for Larch show how one can prove that a procedure specification is protected from the effects of underspecification. @blankspace(2line) @begin(transparent,size=10) @b(Keywords:@ )@c @end(transparent) @blankspace(1line) @end(text) @flushright(@b[(22 pages)])