| |
|
| java.lang.Object U2.T2.MyPerson
MyPerson | public class MyPerson implements Serializable(Code) | | Just a simple class representing a person; used for testing T2
engine.
|
Field Summary | |
public int | age |
Method Summary | |
public boolean | classinv() | public void | makeOlder(int x) Increases the person's age by x. | public void | makeOlder_spec(int x) This specifyies the class invariant; in this case it requires:
age >= 0. |
classinv | public boolean classinv()(Code) | | |
makeOlder | public void makeOlder(int x)(Code) | | Increases the person's age by x. Note that this method does may
violate the given class invariant.
|
makeOlder_spec | public void makeOlder_spec(int x)(Code) | | This specifyies the class invariant; in this case it requires:
age >= 0.
|
|
|
|