Enhancing the Pre- and Postcondition Technique for More Expressive Specifications
Enhancing the Pre- and Postcondition Technique for More Expressive Specifications
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
1 - 1 of 1