Leavens, Gary T. and Baker, Albert L. (1997) Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. Technical Report TR97-19, Department of Computer Science, Iowa State University.
Enhancing the Pre- and Postcondition Technique
for More Expressive Specifications
Gary T. Leavens and Albert L. Baker
We describe enhancements to the pre- and postcondition technique that
help specifications convey reuse contracts more effectively. Some
enhancements also allow one to specify redundant information that can
be used in ``debugging'' specifications. For instance, adding
examples to a specification gives redundant information that may aid
some rusers, and can also be used to help ensure that the
specification says what is intended. Other enhancements allow
improvements in frame axioms for object-oriented (OO) procedures,
better treatments of exceptions and inheritance, and improved
specification of incompletely-specified types.
Several of these enhancements were invented by other authors, but are
not widely known. They have all been integrated into Larch/C++, a
Larch-style behavioral interface specification language for C++.
However, we hope that such enhancements will make any specification
language a more effective tool for reuse.
Keywords: formal methods, liberal specification, redundancy,
debugging, history constraint.
1997 CR Categories:
D.2.1 [Software Engineering]
Requirements/Specifications -- languages, human factors;
D.2.m [Software Engineering]
Miscellaneous -- reusable software;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs --
Pre- and post-conditions, specification techniques.
Contact site administrator at: email@example.com