Improving JML\u27s assignable clause analysis

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