A Runtime Assertion Checker for the Java Modeling Language (JML)

dc.contributor.author Cheon, Yoonsik
dc.contributor.author Leavens, Gary
dc.contributor.department Computer Science
dc.date 2018-02-14T00:00:33.000
dc.date.accessioned 2020-06-30T01:56:12Z
dc.date.available 2020-06-30T01:56:12Z
dc.date.issued 2002-04-01
dc.description.abstract <p>Debugging is made difficult by the need to precisely describe what each piece of the software is supposed to do, and to write code to defend modules against the errors of other modules; if this is not done it is difficult to assign blame to a small part of the program when things go wrong. Similarly, unit testing also needs precise descriptions of behavior, and is made difficult by the need to write test oracles. However, debugging and testing consume a significant fraction of the cost of software development and maintenance efforts. Inadequate debugging and testing also contribute to quality problems. We describe a runtime assertion checker for the Java Modeling Language (JML) that helps in assigning blame during debugging and in automatic generation of test oracles. It represents a significant advance over the current state of the art, because it can deal with very abstract specifications which hide representation details, and other features such as quantifiers, and inheritance of specifications. Yet JML specifications have a syntax that is easily understood by programmers. Thus, JML's runtime assertion checker has the potential for decreasing the cost of debugging and testing.</p>
dc.description.comments <p>To appear in <em>International Conference on Software Engineering Research and Practice</em><em> (SERP) 2002, Las Vegas, Nevada, USA, June 24-27, 2002.</em> Copyright © Computer Science Research, Education, and Application (CSREA) Press, 2002.</p>
dc.identifier archive/lib.dr.iastate.edu/cs_techreports/259/
dc.identifier.articleid 1259
dc.identifier.contextkey 5473697
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/259
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/20082
dc.source.bitstream archive/lib.dr.iastate.edu/cs_techreports/259/tr02_05a.pdf|||Fri Jan 14 22:59:42 UTC 2022
dc.subject.disciplines Software Engineering
dc.subject.keywords runtime assertion checking
dc.subject.keywords formal methods
dc.subject.keywords formal interface specification
dc.subject.keywords programming by contract
dc.subject.keywords JML language
dc.subject.keywords Java language
dc.title A Runtime Assertion Checker for the Java Modeling Language (JML)
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:
tr02_05a.pdf
Size:
85.9 KB
Format:
Adobe Portable Document Format
Description:
Collections