Enhancing the Pre- and Postcondition Technique for More Expressive Specifications







Deposit Papers 


Leavens, Gary T. and Baker, Albert L. (1999) Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. Technical Report TR97-19b, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF


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 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 {\LCC}, 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.
To appear in Jeannette Wing and James Woodcock, editors.
FM'99: World Congress on Formal Methods in Development of Computer Systems,
Toulouse, France, September 1999.  Lecture Notes in Computer Science,
Copyright (c) Springer-Verlag, 1999.

Subjects:All uncategorized technical reports
ID code:00000202
Deposited by:Staff Account on 29 June 1999

Contact site administrator at: