Technical Report Number
Software, Computing Methodologies, Theory of Computation
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.