|
392
|
1 // $HeadURL$
|
|
|
2 // $Date$
|
|
|
3 // $Author$
|
|
|
4
|
|
|
5 module dstress.run.invariant_27;
|
|
|
6
|
|
|
7 int status;
|
|
|
8 int inv;
|
|
|
9
|
|
|
10 class MyClass{
|
|
|
11
|
|
|
12 this(){
|
|
|
13 }
|
|
|
14
|
|
|
15 public static void check(){
|
|
|
16 status++;
|
|
|
17 }
|
|
|
18
|
|
|
19 private void middle(){
|
|
|
20 check();
|
|
|
21 }
|
|
|
22
|
|
|
23 invariant{
|
|
|
24 middle();
|
|
|
25 inv++;
|
|
|
26 }
|
|
|
27 }
|
|
|
28
|
|
|
29 int main(){
|
|
|
30
|
|
|
31 MyClass o;
|
|
|
32 assert(status==0);
|
|
|
33 assert(inv==0);
|
|
|
34
|
|
|
35 o=new MyClass();
|
|
|
36 assert(status==1);
|
|
|
37 assert(inv==1);
|
|
|
38
|
|
|
39 o.check();
|
|
|
40 assert(status==2);
|
|
|
41 assert(inv==1);
|
|
|
42
|
|
|
43 MyClass.check();
|
|
|
44 assert(status==3);
|
|
|
45 assert(inv==1);
|
|
|
46
|
|
|
47 return 0;
|
|
|
48 }
|
