Desugaring JML Method Specifications

dc.contributor.author Raghavan, Arun
dc.contributor.author Leavens, Gary
dc.contributor.department Computer Science
dc.date 2018-02-14T00:59:44.000
dc.date.accessioned 2020-06-30T01:56:52Z
dc.date.available 2020-06-30T01:56:52Z
dc.date.issued 2005-05-01
dc.description.abstract <p>JML, which stands for ``Java Modeling Language,'' is a behavioral interface specification language (BISL) designed to specify Java modules. JML features a great deal of syntactic sugar that is designed to make method specifications more expressive. This paper presents a desugaring process that boils down all of the syntactic sugars in JML method specifications into a much simpler form. This desugaring will help one understand the meaning of these sugars, for example for use in program verification. It may also help manipulation of JML method specifications by tools.</p>
dc.description.comments <p>Copyright © 2000, 2001, 2003, 2005 by Iowa State University</p>
dc.identifier archive/lib.dr.iastate.edu/cs_techreports/345/
dc.identifier.articleid 1344
dc.identifier.contextkey 5542804
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/345
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/20177
dc.source.bitstream archive/lib.dr.iastate.edu/cs_techreports/345/TR.pdf|||Fri Jan 14 23:42:15 UTC 2022
dc.subject.disciplines Software Engineering
dc.subject.disciplines Theory and Algorithms
dc.subject.keywords Behavioral interface specification language
dc.subject.keywords formal specification
dc.subject.keywords desugaring
dc.subject.keywords semantics
dc.subject.keywords specification inheritance
dc.subject.keywords refinement
dc.subject.keywords behavioral subtyping
dc.subject.keywords model-based specification
dc.subject.keywords formal methods
dc.subject.keywords precondition
dc.subject.keywords postcondition
dc.subject.keywords Eiffel
dc.subject.keywords Java
dc.subject.keywords JML
dc.title Desugaring JML Method 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:
TR.pdf
Size:
302.8 KB
Format:
Adobe Portable Document Format
Description:
Collections