archives

Protective Interface Specifications


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T. and Wing, Jeannette M. (1997) Protective Interface Specifications. Technical Report TR96-04c, 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.
Keywords:  Protective specifications;
Specification languages; Underspecification; Partiality; Larch.
1996 CR Categories:
D.2.1 [Software Engineering]
Requirements/Specifications --- languages, theory, Larch, VDM, Z, RESOLVE
D.2.7 [Software Engineering]
Distribution and Maintenance --- documentation;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
assertions, logics of programs, pre- and post-conditions,
specification techniques, theory, LSL

Subjects:All uncategorized technical reports
ID code:00000139
Deposited by:Staff Account on 11 February 1997



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