Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Enhancing the pre- and postcondition technique for more expressive specifications

Gary T. LeavensContact Information and Albert L. BakerContact Information

(6)  Department of Computer Science, Iowa State University, 226 Atanasoff Hall, Ames, Iowa 50011-1040, USA
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 Larchstyle behavioral interface specification language for C++. However, such enhancements could also be used to make other specification languages more effective tools for communication.

Keywords  specification language design - expressiveness - liberal specification - redundancy - debugging - history constraint - Larch


Contact Information Gary T. Leavens
Email: leavens@cs.iastate.edu
URL: http://www.cs.iastate.edu/~leavens/index.html

Contact Information Albert L. Baker
Email: baker@cs.iastate.edu
URL: http://www.cs.iastate.edu/~baker/baker.html
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Referenced by
1 newer article

  1. Cheon, Yoonsik (2005) Model variables: cleanly supporting abstraction in design by contract. Software Practice and Experience 35(6)
    [CrossRef]
Remote Address: 38.107.191.106 • Server: MPWEB25
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)