Improving JML's assignable clause analysis

Thumbnail Image
Date
2006-07-01
Authors
Ye, Cui
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Organizational Unit
Journal Issue
Is Version Of
Versions
Series
Department
Computer Science
Abstract

The Java Modeling Language (JML) is a formal behavioral interface specification language (BISL) for Java. Its RAC tool (jmlc) performs runtime assertion checking by embedding assertions that check user specifications into the source code compiled for user program. Reasoning about state changes, that is, about side effects, is crucial to reasoning about programs. Such reasoning further affects proving program correctness and analyzing interesting properties. In JML, the assignable clause is for the purpose of specifying possible side effects that could happen in a method. This thesis work focuses on making sure that the assignable clause is checked appropriately by jmlc. To perform the assignable clause checking, we combine runtime and static checking. The runtime checking follows the fashion of current jmlc. It generates assertions that check whether certain side effects are allowed in a method and embeds them into user programs. These assertions are checked at runtime. Meanwhile, the static checking collects useful predicates appearing in the method�s source code, and its strategy is to use the available predicate environments to prove target assertion predicates at the points right before embedding the target assertions into user programs. Examples of useful predicates are if-conditions, loop tests, predicates of assertions appearing in a method, etc. If the static checking could prove the target assertion, then there is no need to go on with the rest of runtime checking. Otherwise, the tool continues with inserting the assertion. The runtime checking improves the precision, while the static one improves runtime performance.

Comments

Copyright © 2006 by Cui Ye

Description
Keywords
Citation
DOI
Source
Copyright
Collections