ChAsE

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 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

Example

Package utils

Package pacapinterfaces

Package purse