ChAsE

ChAsE, which is short for Check Assignable Expression can be used for static checking of JML's assignable clauses. It has been developed by Néstor Cataño at INRIA Sophia-Antipolis as part of the Verificard project.

ChAsE allows to check whether the side-effects of a Java method are correctly specified, and in particular whether a method is pure. The tool uses a syntactic method to check assignable clauses, and it is neither sound nor complete, but intended to be practical -- because it can find the most common errors in assignable clauses very efficiently. ChAsE is an extension of ESC/Java, a static checker for Java programs, which in its current state does not check assignable clauses at all.

The current implementation of ChAsE can check assignable clauses containing assignable expressions as described by the following grammar (model variables are not handled).

<Assignable-exp> ::= <Identifier> 
                   | <Identifier>[Exp] 
                   | <Identifier>[Exp .. Exp]  
                   | <Identifier>[*] 
                   | \fields\_of(<Field-exp>)  
                   | \nothing 
                   | \everything 

<Field-exp> ::= <Point-identif>  
              | this 
              | \reach(<Point-identif>)  
              | reach(this)  

<Point-identif> ::= <Identifier>.<Point-identif>  
                  | <Identifier>
ChAsE  and the specifications we constructed for Formal specification of Gemplus' electronic purse case study  can be downloaded from here. When you unzip and untar this file, you will find instructions in the file README.txt.

ChAsE and the underlying method will be described in the paper A static checker for JML's assignable clause, by Néstor Cataño and Marieke Huisman (manuscript).

Questions

If you have any questions concerning the use of ChAsE, you can contact Néstor Cataño.

Example

To illustrate the use of ChAsE, we have checked the assignable clauses that we have developed in an earlier case study on specification and static checking of an electronic purse applet. In order to focus on the assignable clause, we have eliminated all other parts of the specification. The assignable clauses that we initially had forgotten to specify are marked with !! (see also the remarks).

Package utils

Classname Remarks
Annee 1 side-effects free method 
Jour 1 side-effects free method 
Mois 1 side-effects free method 
PacapException 1 side-effects free method 
DecimalException
Decimal 12 side-effects free methods, 9 specification problems found 

Package pacapinterfaces

Classname Remarks
LoyaltyLoyaltyInterface 2 side-effects free methods 
LoyaltyPurseInterface 2 side-effects free methods 
PurseLoyaltyInterface 4 side-effects free methods 
TransactionInterface 10 side-effects free methods 

Package purse

Classname Remarks
DateException
Date 5 side-effects free methods, 2 specification problems found in 2 methods 
HeureException
Heure 2 side-effects free methods, 2 specification problems found in 2 methods 
PartnerID 1 side-effects free method 
SalerID 1 side-effects free method, 4 specification problems found in 3 methods
LoyaltiesTableException
LoyaltiesTable 4 side-effects free methods 
AllowedLoyaltyException
AllowedLoyalty 6 side-effects free methods, 3 specification problems found in 3 methods
AccessConditionException
AccessCondition 4 side-effects free methods 
AccessControlTable 2 side-effects free methods 
AccessControl 1 side-effects free method 
Currencies 3 side-effects free methods 
ExchangeSession 10 side-effects free methods, 7 specification problems found in 4 methods 
ExchangeRecord 5 side-effects free methods, 16 specification problems found in 2 methods