Improving JML's assignable clause analysis







Deposit Papers 


Ye, Cui (2006) Improving JML's assignable clause analysis. Technical Report TR06-19, Computer Science, Iowa State University.

Full text available as:Adobe PDF


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.

Keywords:JML, frame axiom, modifies clause, assignable clause, runtime assertion checking, static analysis, intraprocedural analysis, interprocedural analysis, precondition, assignable field set, flow predicate, precision, safety.
Comments:Cui Ye's MS thesis.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
ID code:00000439
Deposited by:Gary T. Leavens on 01 August 2006
Alternative Locations:

Contact site administrator at: