A runtime assertion checker for the Java Modeling Language

dc.contributor.advisor Gary T. Leavens
dc.contributor.author Cheon, Yoonsik
dc.contributor.department Computer Science
dc.date 2018-08-24T19:58:14.000
dc.date.accessioned 2020-07-02T05:49:50Z
dc.date.available 2020-07-02T05:49:50Z
dc.date.copyright Wed Jan 01 00:00:00 UTC 2003
dc.date.issued 2003-01-01
dc.description.abstract <p>The Java Modeling Language (JML) is a formal behavioral interface specification language (BISL) for Java. JML has many advances including specification-only declarations, specifications of interfaces, stateful interfaces, multiple inheritance of specifications, and behavioral subtyping. An approach to runtime assertion checking of JML assertions is presented and implemented as a JML compiler to translate Java programs annotated with JML specifications into Java bytecode. The compiled bytecode transparently checks JML specifications at runtime. The JML compiler supports separate and modular compilation. The approach brings programming benefits such as debugging and testing to BISLs and also helps programmers to use BISLs in their daily programming.;A set of translation rules are defined from JML expressions into assertion checking code. The translation rules handle various kinds of undefinedness, such as runtime exceptions and non-executable constructs, in such a way as to both satisfy the standard rules of logic and detect as many assertion violations as possible. The rules also support various forms of quantifiers. Specification-only declarations such as model fields, ghost fields, and model methods are translated into access methods; e.g., an access method for a model field is an abstraction function that calculates an abstract value from the program state. The specification state of a stateful interface, due to specification-only fields such as ghost fields, is represented as a separate assertion class. Thus, an object's specification state is distributed over the object itself and one assertion object for each interface that its class implements. Assertion checking is also distributed in that a subtype delegates the responsibility of checking inherited specifications to its supertypes (or the assertion classes of its superinterfaces). The delegation approach supports multiple inheritance, and is modular.;Finally, the effectiveness and practicality of runtime assertion checking is demonstrated by applying it to program testing. An approach is implemented that significantly automates unit testing. The key idea of the approach is to view interface specifications as test oracles and to use the runtime assertion checker as the decision procedure of the test oracles. The approach also shows that the runtime assertion checker can be an effective framework for developing specification-based tools.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/rtd/570/
dc.identifier.articleid 1569
dc.identifier.contextkey 6075511
dc.identifier.doi https://doi.org/10.31274/rtd-180813-9872
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath rtd/570
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/78385
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/rtd/570/r_3085895.pdf|||Sat Jan 15 00:59:18 UTC 2022
dc.subject.disciplines Computer Sciences
dc.subject.keywords Computer science
dc.title A runtime assertion checker for the Java Modeling Language
dc.type article
dc.type.genre dissertation
dspace.entity.type Publication
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
thesis.degree.level dissertation
thesis.degree.name Doctor of Philosophy
Original bundle
Now showing 1 - 1 of 1
5.36 MB
Adobe Portable Document Format