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. (1999) Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. Technical Report TR97-19a, 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 information more effectively.  Some
enhancements 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
readers, 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 support for
incompletely-specified types.
Many 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, such enhancements could also be used to make other
specification languages more effective tools for communication.
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:00000199
Deposited by:Staff Account on 10 February 1999



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