Leavens, Gary T. and Wing, Jeannette M. (1997) Protective Interface Specifications. Technical Report TR96-04d, Department of Computer Science, Iowa State University.
Protective Interface Specifications
Gary T. Leavens and Jeannette M. Wing
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
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
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
Contact site administrator at: firstname.lastname@example.org