| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | """Support Eiffel-style preconditions and postconditions.
 | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | For example, | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | class C: | 
					
						
							|  |  |  |     def m1(self, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         require arg > 0 | 
					
						
							|  |  |  |         return whatever | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  |         ensure Result > arg | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | can be written (clumsily, I agree) as: | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | class C(Eiffel): | 
					
						
							|  |  |  |     def m1(self, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         return whatever | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  |     def m1_pre(self, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         assert arg > 0 | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  |     def m1_post(self, Result, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         assert Result > arg | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | 
 | 
					
						
							|  |  |  | Pre- and post-conditions for a method, being implemented as methods | 
					
						
							|  |  |  | themselves, are inherited independently from the method.  This gives | 
					
						
							|  |  |  | much of the same effect of Eiffel, where pre- and post-conditions are | 
					
						
							|  |  |  | inherited when a method is overridden by a derived class.  However, | 
					
						
							|  |  |  | when a derived class in Python needs to extend a pre- or | 
					
						
							|  |  |  | post-condition, it must manually merge the base class' pre- or | 
					
						
							|  |  |  | post-condition with that defined in the derived class', for example: | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | class D(C): | 
					
						
							|  |  |  |     def m1(self, arg): | 
					
						
							| 
									
										
										
										
											2002-07-11 20:22:11 +00:00
										 |  |  |         return arg**2 | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  |     def m1_post(self, Result, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         C.m1_post(self, Result, arg) | 
					
						
							|  |  |  |         assert Result < 100 | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | 
 | 
					
						
							|  |  |  | This gives derived classes more freedom but also more responsibility | 
					
						
							|  |  |  | than in Eiffel, where the compiler automatically takes care of this. | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | In Eiffel, pre-conditions combine using contravariance, meaning a | 
					
						
							|  |  |  | derived class can only make a pre-condition weaker; in Python, this is | 
					
						
							|  |  |  | up to the derived class.  For example, a derived class that takes away | 
					
						
							|  |  |  | the requirement that arg > 0 could write: | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  |     def m1_pre(self, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         pass | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | 
 | 
					
						
							|  |  |  | but one could equally write a derived class that makes a stronger | 
					
						
							|  |  |  | requirement: | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  |     def m1_pre(self, arg): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         require arg > 50 | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | 
 | 
					
						
							|  |  |  | It would be easy to modify the classes shown here so that pre- and | 
					
						
							|  |  |  | post-conditions can be disabled (separately, on a per-class basis). | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | A different design would have the pre- or post-condition testing | 
					
						
							|  |  |  | functions return true for success and false for failure.  This would | 
					
						
							|  |  |  | make it possible to implement automatic combination of inherited | 
					
						
							|  |  |  | and new pre-/post-conditions.  All this is left as an exercise to the | 
					
						
							|  |  |  | reader. | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | """
 | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | from Meta import MetaClass, MetaHelper, MetaMethodWrapper | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | class EiffelMethodWrapper(MetaMethodWrapper): | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  |     def __init__(self, func, inst): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         MetaMethodWrapper.__init__(self, func, inst) | 
					
						
							|  |  |  |         # Note that the following causes recursive wrappers around | 
					
						
							|  |  |  |         # the pre-/post-condition testing methods.  These are harmless | 
					
						
							|  |  |  |         # but inefficient; to avoid them, the lookup must be done | 
					
						
							|  |  |  |         # using the class. | 
					
						
							|  |  |  |         try: | 
					
						
							|  |  |  |             self.pre = getattr(inst, self.__name__ + "_pre") | 
					
						
							|  |  |  |         except AttributeError: | 
					
						
							|  |  |  |             self.pre = None | 
					
						
							|  |  |  |         try: | 
					
						
							|  |  |  |             self.post = getattr(inst, self.__name__ + "_post") | 
					
						
							|  |  |  |         except AttributeError: | 
					
						
							|  |  |  |             self.post = None | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | 
 | 
					
						
							|  |  |  |     def __call__(self, *args, **kw): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         if self.pre: | 
					
						
							|  |  |  |             apply(self.pre, args, kw) | 
					
						
							|  |  |  |         Result = apply(self.func, (self.inst,) + args, kw) | 
					
						
							|  |  |  |         if self.post: | 
					
						
							|  |  |  |             apply(self.post, (Result,) + args, kw) | 
					
						
							|  |  |  |         return Result | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  |      | 
					
						
							|  |  |  | class EiffelHelper(MetaHelper): | 
					
						
							|  |  |  |     __methodwrapper__ = EiffelMethodWrapper | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | class EiffelMetaClass(MetaClass): | 
					
						
							|  |  |  |     __helper__ = EiffelHelper | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | Eiffel = EiffelMetaClass('Eiffel', (), {}) | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  | def _test(): | 
					
						
							|  |  |  |     class C(Eiffel): | 
					
						
							| 
									
										
										
										
											1998-09-14 16:44:15 +00:00
										 |  |  |         def m1(self, arg): | 
					
						
							|  |  |  |             return arg+1 | 
					
						
							|  |  |  |         def m1_pre(self, arg): | 
					
						
							|  |  |  |             assert arg > 0, "precondition for m1 failed" | 
					
						
							|  |  |  |         def m1_post(self, Result, arg): | 
					
						
							|  |  |  |             assert Result > arg | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  |     x = C() | 
					
						
							|  |  |  |     x.m1(12) | 
					
						
							| 
									
										
										
										
											1997-08-26 00:08:51 +00:00
										 |  |  | ##    x.m1(-1) | 
					
						
							| 
									
										
										
										
											1997-08-25 15:37:59 +00:00
										 |  |  | 
 | 
					
						
							|  |  |  | if __name__ == '__main__': | 
					
						
							|  |  |  |     _test() |