archives

Enhancing the Pre- and Postcondition Technique for More Expressive Specifications


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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.

Full text available as:Postscript
Adobe PDF

Abstract

Enhancing the Pre- and Postcondition Technique
for More Expressive Specifications
by
Gary T. Leavens and Albert L. Baker
Abstract
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.

Subjects:All uncategorized technical reports
ID code:00000160
Deposited by:Staff Account on 19 September 1997



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