public class Person {
    private /*@ spec_public non_null @*/
        String name;
    private /*@ spec_public @*/
        int weight;

    /*@ public invariant !name.equals("")
      @               && weight >= 0;
      @*/

    //@ also
    //@ ensures \result != null;
    public String toString() {
	return "Person(\""
            + name + "\"," + weight + ")";
    }

    /*@ ensures \result == weight;
      @*/
    public /*@ pure @*/ int getWeight() {
        return weight;
    }

    /*@ ensures kgs >= 0
      @      && weight
      @          == \old(weight + kgs);
      @ signals (IllegalArgumentException e)
      @         kgs < 0;
      @*/
    public void addKgs(int kgs) {
        weight += kgs; //error...
    }
    
    /*@ requires n != null
      @       && !n.equals("");
      @ ensures n.equals(name)
      @      && weight == 0;
      @*/
    public Person(String n) {
       name = n; weight = 0;
    }
}