// openjml --esc Age.java
public interface Age {
    //@ model instance int age;
    //@ public invariant 0 <= age;
}