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-04d, 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.
An earlier version of this paper, without the appendix sections,
appeared in Michel Bidoit and Max Dauchet (editors),
TAPSOFT '97: Theory and Practice of Software Development,
7th International Joint Conference CAAP/FASE, Lille, France.
Volume 1214 of Lecture Notes in Computer Science,
Springer-Verlag, 1997, pages 520-534.
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:00000159
Deposited by:Staff Account on 16 September 1997



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