Adding native specications to JML

Abstract. In the specication language JML we can see pure methods as a way to express user-dened predicates that will simplify the anno-tations. We take this idea a step further in allowing to only declare these predicates in JML without giving an explicit denition. The explicit def-inition is done directly in the language to which the Java program an