[Python-Dev] Introduction

Pat Miller patmiller@llnl.gov
Wed, 28 May 2003 14:01:24 -0700


> http://www.wayforward.net/pycontract/pep-0999.html

I think another issue with using doc strings in this way
is that you are overloading a feature visible to end users.

If I look at the doc string then I would expect to be confused the result:

 >>> help(circbuf)
Help on class circbuf in module __main__:

class circbuf
  |  Methods defined here:
  |
  |  get(self)
  |      Pull an entry from a non-empty circular buffer.
  |
  |      pre: not self.is_empty()
  |      post[self.g, self.len]:
  |          __return__ == self.buf[__old__.self.g]
  |          self.len == __old__.self.len - 1
  | ...

Way to cryptic even for me :-)

I think you could get the same effect by overloading property
so you could make methods "smart" about pre and post conditions
The following is a first quick hack at it...:

class eiffel(property):
     """eiffel(method,precondition,postcondition)

     Implement a Eiffel style method that enforces pre-
     and post- conditions.  I guess you could turn this
     on and off if you wanted...

     class foo:
       def pre(self): assert self.x > 0
       def post(self):  assert self.x > 0
       def increment(self):
           self.x += 1
           return

       increment = eiffel(method,precondition,postcondition)
     """

     def __init__(self,method,precondition,postcondition,doc=None):
	self.method	= method
	self.precondition	= precondition
	self.postcondition	= postcondition
         super(eiffel,self).__init__(self.__get,None,None,doc)
	return


     def __get(self,this):
         class funny_method:
             def __init__(self,this,method,precondition,postcondition):
                 self.this	= this
                 self.method	= method
                 self.precondition	= precondition
                 self.postcondition	= postcondition
                 return
             def __call__(self,*args,**kw):
                 self.precondition(self.this)
                 value = self.method(self.this,*args,**kw)
                 self.postcondition(self.this)
                 return value

         return funny_method(this,self.method,self.precondition,self.postcondition)



class circbuf:
     def __init__(self):
         self.stack = []
         return

     def _get_pre(self):
         assert not self.is_empty()
         return
     def _get_post(self):
         assert not self.is_empty()
         return
     def _get(self):
         """Pull an entry from a non-empty circular buffer."""
         val = self.stack[-1]
         del self.stack[-1]
         return val

     get = eiffel(_get,_get_pre,_get_post)

     def put(self,val):
         self.stack.append(val)
         return

     def is_empty(self):
         return len(self.stack) == 0


B = circbuf()
B.put('hello')
print B.get()

# Will bomb...
print B.get()


-- 
Patrick Miller | (925) 423-0309 | http://www.llnl.gov/CASC/people/pmiller

If you think you can do a thing or think you can't do a thing, you're
right.  -- Henry Ford