DISCLAIMER

I wrote this software only as a test to see how far can I push Python. I DO NOT intend to use it in a production environment, nor do I advice anyone of doing so - it is probably really slow and no one actually needs runtime checking of pre- and postconditions for Python. I will not be responsible for anything happening due to use of this project. Read the BSD License for more information.

INTRODUCTION

This package contains simple to use invariants, preconditions and postconditions for Python 3. It consists of a class (which should be used as the metaclass of the class you want to use annotations in) and some decorators, defined in it. All of this was necessary, because I wanted the cleanliest solution - you will see in the example. Python 3 IS needed, because I am using __prepare__, which is a new feature there. Here is a simple example of what is possible and how it works:

from DbC import DbC

class Test(metaclass = DbC):
    
    @invar(x >= 0)
    
    def __init__(self, x):
        self.x = x

    @pre(x >= 0)
    @post(res == x + 1)
    def foo(self, x):
        result = x + self.x
        self.x -= 2
        return result

    @staticmethod
    @pre(len(list(map(lambda x: x + 2, filter(lambda y: y == 0, z + [0])))) == 1)
    def bar(z):
        pass

t = Test(1)
t.foo(3)
Test.bar([1, 2, 3])


This will fail with "Invariants failed after function: foo" on the second to last line, because the invariant is for self.x to be >= 0, but it becomes -1 in foo. There are a few things to note here.

As I said, I like the "cleanliness" of the use - there are no strings in the conditions, there are no other variable names. You just use the same name of the argument, as if you were inside the function itself. And, besides, it looks nice. :)

Invariants, pre- and postconditions are all decorators. The invariants decorator you could put anywhere, it doesn't matter (except "above" other, non-DbC decorators - see below). I prefer to keep them separeted (as if they weren't a decorator to a function but just syntax), above the constructor. Inside them you can use any variable name that is an instance variable. Obviously, you HAVE to declare all instance variables that are used in invariants in __init__, otherwise it will blow up after the constructor. I think this is the "right" way, because otherwise you might have an invariant which uses a variable with a typo and it would never be called, waiting for the variable to be declared somewhere. In invariants you do not use self (or whatever the name of your first arguments is) before the variable names.

Preconditions are pretty much the same, except you can name function arguments instead of instance vars. This time, if you want to access instance vars, you have to go through your first argument - e.g. self.x > 0.

The same things go for the postconditions, except that you have a special variable, named "res" which stands for your result. Note that if you have a parameter, called res, IT is going to be used, not the result from the function. Another thing is that the parameter values are the INITIAL ones, so you can compare the result to them.

Obviously, you can use in all these any built-in function or things from the outer scope. Any number of invar's, pre- and postconditions are allowed, and in any order. See the more detailed example for... an example. :)

Staticmethod and classmethod decorators work. This is done by some descriptor forwarding and currying. Note that the static/classmethod decorator should come LAST of all (that is, "on top"), otherwise it wouldn't work (this is because they return descriptor objects, which means I would have to emulate them and thus lose the ability to return a wrapped function looking just like the method itself). The three DbC decorators all returning wrapped functions means that you probably could use them with other decorators AFTER that (like the static/classmethod ones - ABOVE the DbC ones). This maybe could work even better if one uses the decorator module instead of the built-in "wrap", but I decided not to go with it. You could try.

There are a bunch of operators you can use in the invariants and *conditions, but I have probably missed a few. These are trivial to add. A note - instead of "and" and "or", you should use operators "&" and "|", otherwise it wouldn't work. Don't worry, they short-circuit. :)

Unfortunatelly I couldn't make argument names to be used in lambda functions in the invars/*conds. I think it may be possible by playing with the code of the lambdas and "low-level" stuff like that or by using exec with the correct dictionaries, but I won't bother. Unfortunatelly, as of Python 3.1.2, giving values to the free variables of a function is not allowed, at least not through the simple accessors it has.

I think that pretty much covers it. Feel free to download the code, go through it, play with it and if you come up with something interesting, let me know!

Last edited Apr 1, 2010 at 6:44 PM by Alien282, version 2

Comments

No comments yet.