// @(#)$Id: Person.refines-java,v 1.6 2005/08/24 20:45:58 leavens Exp $ // Copyright (C) 2003 Iowa State University // This file is part of JML // JML is free software; you can redistribute it and/or modify // it under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 2, or (at your option) // any later version. // JML is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU General Public License for more details. // You should have received a copy of the GNU General Public License // along with JML; see the file COPYING. If not, write to // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA. package org.jmlspecs.samples.jmltutorial; //@ refine "Person.java"; 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(); //@ also //@ ensures \result == weight; public /*@ pure @*/ int getWeight(); /*@ also @ requires kgs >= 0; @ requires weight + kgs >= 0; @ ensures weight == \old(weight + kgs); @*/ public void addKgs(int kgs); /*@ also @ requires n != null && !n.equals(""); @ ensures n.equals(name) @ && weight == 0; @*/ public Person(String n); }