Static Analysis for JML's assignable Clauses