• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
1"""Support Eiffel-style preconditions and postconditions.
2
3For example,
4
5class C:
6    def m1(self, arg):
7        require arg > 0
8        return whatever
9        ensure Result > arg
10
11can be written (clumsily, I agree) as:
12
13class C(Eiffel):
14    def m1(self, arg):
15        return whatever
16    def m1_pre(self, arg):
17        assert arg > 0
18    def m1_post(self, Result, arg):
19        assert Result > arg
20
21Pre- and post-conditions for a method, being implemented as methods
22themselves, are inherited independently from the method.  This gives
23much of the same effect of Eiffel, where pre- and post-conditions are
24inherited when a method is overridden by a derived class.  However,
25when a derived class in Python needs to extend a pre- or
26post-condition, it must manually merge the base class' pre- or
27post-condition with that defined in the derived class', for example:
28
29class D(C):
30    def m1(self, arg):
31        return arg**2
32    def m1_post(self, Result, arg):
33        C.m1_post(self, Result, arg)
34        assert Result < 100
35
36This gives derived classes more freedom but also more responsibility
37than in Eiffel, where the compiler automatically takes care of this.
38
39In Eiffel, pre-conditions combine using contravariance, meaning a
40derived class can only make a pre-condition weaker; in Python, this is
41up to the derived class.  For example, a derived class that takes away
42the requirement that arg > 0 could write:
43
44    def m1_pre(self, arg):
45        pass
46
47but one could equally write a derived class that makes a stronger
48requirement:
49
50    def m1_pre(self, arg):
51        require arg > 50
52
53It would be easy to modify the classes shown here so that pre- and
54post-conditions can be disabled (separately, on a per-class basis).
55
56A different design would have the pre- or post-condition testing
57functions return true for success and false for failure.  This would
58make it possible to implement automatic combination of inherited
59and new pre-/post-conditions.  All this is left as an exercise to the
60reader.
61
62"""
63
64from Meta import MetaClass, MetaHelper, MetaMethodWrapper
65
66class EiffelMethodWrapper(MetaMethodWrapper):
67
68    def __init__(self, func, inst):
69        MetaMethodWrapper.__init__(self, func, inst)
70        # Note that the following causes recursive wrappers around
71        # the pre-/post-condition testing methods.  These are harmless
72        # but inefficient; to avoid them, the lookup must be done
73        # using the class.
74        try:
75            self.pre = getattr(inst, self.__name__ + "_pre")
76        except AttributeError:
77            self.pre = None
78        try:
79            self.post = getattr(inst, self.__name__ + "_post")
80        except AttributeError:
81            self.post = None
82
83    def __call__(self, *args, **kw):
84        if self.pre:
85            apply(self.pre, args, kw)
86        Result = apply(self.func, (self.inst,) + args, kw)
87        if self.post:
88            apply(self.post, (Result,) + args, kw)
89        return Result
90
91class EiffelHelper(MetaHelper):
92    __methodwrapper__ = EiffelMethodWrapper
93
94class EiffelMetaClass(MetaClass):
95    __helper__ = EiffelHelper
96
97Eiffel = EiffelMetaClass('Eiffel', (), {})
98
99
100def _test():
101    class C(Eiffel):
102        def m1(self, arg):
103            return arg+1
104        def m1_pre(self, arg):
105            assert arg > 0, "precondition for m1 failed"
106        def m1_post(self, Result, arg):
107            assert Result > arg
108    x = C()
109    x.m1(12)
110##    x.m1(-1)
111
112if __name__ == '__main__':
113    _test()
114