Improving JML's assignable clause analysis
                                  by
				Cui Ye

			       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.

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.

2006 CR Categories:
D.2.1 [Software Engineering]
    Requirements Specifications --- languages;
D.2.4 [Software Engineering]
    Software/Program Verification --- assertion checkers,
    formal methods, programming by contract;
F.3.1 [Logics and Meanings of Programs]
    Specifying and Verifying and Reasoning about Programs ---
    assertions, logics of programs, mechanical
    verification, pre- and post-conditions, specification techniques;
F.3.2 [Logics and Meanings of Programs]
    Semantics of Programming Languages --- program analysis.