blob: d8cd4d3f05eb50b1130aa8fd60d1c7f89d46d930 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
class Foo {
public bool ensured = false;
public bool required = false;
public Foo () requires (required = true) {
}
public Foo.post () ensures (ensured = true) {
}
public void foo () ensures (ensured = true) {
}
public string bar () ensures (result.length >= 3) {
return "bar";
}
public void foo_pre (int i) requires (i > 23) {
assert (i == 42);
}
public int bar_pre (int i) requires (i > 42) {
assert (i == 4711);
return i;
}
public int faz (int i) ensures (result > 23) {
switch (i) {
case 42:
return i;
default:
assert_not_reached ();
}
}
public int faz_pre (int i) requires (i > 23) {
switch (i) {
case 4711:
return i;
default:
assert_not_reached ();
}
}
public virtual int manam (int i) ensures (result > 23) {
switch (i) {
case 67:
return i;
default:
assert_not_reached ();
}
}
public virtual int manam_pre (int i) requires (i > 23) {
switch (i) {
case 231:
return i;
default:
assert_not_reached ();
}
}
}
struct Bar {
public bool ensured;
public bool required;
public Bar () requires (required = true) {
}
public Bar.post () ensures (ensured = true) {
}
public void bar () ensures (ensured = true) {
}
public string foo () ensures (result.length >= 3) {
return "foo";
}
}
void main () {
var foo = new Foo();
assert(foo.required);
foo.foo();
assert(foo.ensured);
assert(foo.bar () == "bar");
foo.foo_pre (42);
assert(foo.bar_pre (4711) == 4711);
assert (foo.faz (42) == 42);
assert (foo.faz_pre (4711) == 4711);
assert (foo.manam (67) == 67);
assert (foo.manam_pre (231) == 231);
var foo2 = new Foo.post ();
assert (foo2.ensured);
var bar = new Bar ();
assert (bar.required);
bar.bar ();
assert (bar.ensured);
assert (bar.foo () == "foo");
var bar2 = new Bar.post ();
assert (bar2.ensured);
}
|
