archives

Protective Interface Specifications


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T. and Wing, Jeannette M. (1996) Protective Interface Specifications. Technical Report TR96-04a, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF

Abstract

Protective Interface Specifications
by
Gary T. Leavens and Jeannette M. Wing
Abstract
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 like VDM-SL and COLD-K.  We also formalize
the notion of protection from underspecification for the Larch family
of specification languages, and for Larch show how one can prove that
a procedure specification is protected from the effects of
underspecification.

Subjects:All uncategorized technical reports
ID code:00000132
Deposited by:Staff Account on 14 October 1996



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