Enhancing the Pre- and Postcondition Technique for More Expressive Specifications

Simple item page
dc.contributor.author Leavens, Gary
dc.contributor.author Baker, Albert
dc.contributor.department Computer Science
dc.date 2018-02-13T22:47:47.000
dc.date.accessioned 2020-06-30T01:55:17Z
dc.date.available 2020-06-30T01:55:17Z
dc.date.issued 1999-02-01
dc.description.abstract <p>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.</p>
dc.description.comments <p>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. <em>Lecture notes in Computer Science</em>, Copyright © Springer-Verlag, 1999.</p>
dc.identifier archive/lib.dr.iastate.edu/cs_techreports/138/
dc.identifier.articleid 1103
dc.identifier.contextkey 5337995
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/138
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/19948
dc.source.bitstream archive/lib.dr.iastate.edu/cs_techreports/138/TR97_19b.pdf|||Fri Jan 14 20:01:04 UTC 2022
dc.subject.disciplines Programming Languages and Compilers
dc.subject.disciplines Systems Architecture
dc.subject.keywords formal methods
dc.subject.keywords liberal specification
dc.subject.keywords redundancy
dc.subject.keywords debugging
dc.subject.keywords history constraint
dc.title Enhancing the Pre- and Postcondition Technique for More Expressive Specifications
dc.type article
dc.type.genre article
dspace.entity.type Publication
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
File
Original bundle
Now showing 1 - 1 of 1
Name:
TR97_19b.pdf
Size:
195.47 KB
Format:
Adobe Portable Document Format
Description:
Download
Collections
Publications