Preliminary Design of JML: A Behavioral Interface Specification Language for Java

dc.contributor.author Leavens, Gary
dc.contributor.author Baker, Albert
dc.contributor.author Ruby, Clyde
dc.contributor.department Computer Science
dc.date 2018-02-13T23:21:19.000
dc.date.accessioned 2020-06-30T01:55:53Z
dc.date.available 2020-06-30T01:55:53Z
dc.date.issued 2006-01-01
dc.description.abstract <p>JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid verification and debugging. JML is designed to be used by working software engineers; to do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions. This paper discusses the goals of JML, the overall approach, and describes the basic features of the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions.</p>
dc.description.comments <p>Copyright © 1998-2006 Iowa State University</p> <p>This document is part of JML and is distributed under the terms of the GNU General Public License as published by the Free Sofware Foundation; either version 2, or (at your option) any later version.</p>
dc.identifier archive/lib.dr.iastate.edu/cs_techreports/216/
dc.identifier.articleid 1187
dc.identifier.contextkey 5436431
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/216
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/20035
dc.source.bitstream archive/lib.dr.iastate.edu/cs_techreports/216/prelimdesign.pdf|||Fri Jan 14 22:38:15 UTC 2022
dc.subject.disciplines Software Engineering
dc.subject.disciplines Theory and Algorithms
dc.subject.keywords Behavioral interface specification
dc.subject.keywords Java
dc.subject.keywords JML
dc.subject.keywords Eiffel
dc.subject.keywords Larch
dc.subject.keywords model-based specification
dc.subject.keywords assertion
dc.subject.keywords precondition
dc.subject.keywords postcondition
dc.subject.keywords frame
dc.title Preliminary Design of JML: A Behavioral Interface Specification Language for Java
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:
prelimdesign.pdf
Size:
564.32 KB
Format:
Adobe Portable Document Format
Description:
Collections