Enhancing the pre- and postcondition technique for more expressive specifications

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