01: package U2.T2;
02:
03: import java.io.*;
04:
05: /**
06: * Just a simple class representing a person; used for testing T2
07: * engine.
08: *
09: */
10: public class MyPerson implements Serializable {
11:
12: private String name;
13: public int age;
14:
15: public MyPerson(String n) {
16: name = n;
17: age = 0;
18: }
19:
20: /**
21: * Increases the person's age by x. Note that this method does may
22: * violate the given class invariant.
23: */
24: public void makeOlder(int x) {
25: age = age + x;
26: // System.out.println("age= " + age) ;
27: }
28:
29: /**
30: * This specifyies the class invariant; in this case it requires:
31: * age >= 0.
32: *
33: */
34: public void makeOlder_spec(int x) {
35: assert x >= -100 : "PRE";
36: makeOlder(x);
37: assert age >= 0 : "POST";
38: }
39:
40: public boolean classinv() {
41: // debug:
42: // System.out.println("#" + name + ", age:" + age) ;
43: return age >= 0;
44: }
45:
46: // note the the method makeOlder does not satisfy this class invariant.
47:
48: }
|