Desugaring JML Method Specifications Raghavan, Arun Leavens, Gary
dc.contributor.department Computer Science 2018-02-14T00:59:44.000 2020-06-30T01:56:52Z 2020-06-30T01:56:52Z 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/
dc.identifier.articleid 1344
dc.identifier.contextkey 5542804
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/345
dc.source.bitstream archive/|||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
Original bundle
Now showing 1 - 1 of 1
302.8 KB
Adobe Portable Document Format