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
|
#!/usr/bin/env python
"""
Tests undefined preconditions on superclasses.
>>> b = B()
>>> b.method(4)
4
>>> b.method(6)
Traceback (most recent call last):
...
PreconditionViolationError: ('testdbca.B.method', 3)
>>> d1 = D1()
>>> d1.method(4)
8
>>> d1.method(6)
Traceback (most recent call last):
...
PreconditionViolationError: ('testdbca.B.method', 3)
>>> d2 = D2()
>>> d2.method(4)
12
>>> d2.method(6)
18
"""
G = 5
class B:
def method(self, a):
"""Contracts
pre: a < 5
post: a <= G
"""
global G
G = a
return a
class D1(B):
def method(self, a):
"""
pre:
a < 6
B.method.__assert_pre(self, a)
"""
global G
G = a * 2
return a * 2
class D2(B):
def method(self, a):
global G
G = a * 3
return a * 3
def _test():
import contract, doctest, testdbca
contract.checkmod(testdbca)
return doctest.testmod(testdbca)
if __name__ == '__main__':
t = _test()
if t[0] == 0:
print "test: %d tests succeeded" % t[1]
else:
print "test: %d/%d tests failed" % t
|
