There are probably a dozen DBC packages on PyPI, and dozens more that never even got that far. If this is doable without language changes, surely it'll be done on PyPI first, get traction there, and only then be considered for inclusion in the stdlib (so that it can be used to contractify parts of the stdlib), right? But, since this is fun: On Jan 26, 2016, at 07:24, Chris Angelico <rosuav@gmail.com> wrote:
On Wed, Jan 27, 2016 at 2:06 AM, Paul Moore <p.f.moore@gmail.com> wrote: Well, classes can be callable already, so how about
@DBC class myfunction: def __call__(self, args): ... @precondition def requires(self): ... @postcondition def ensures(self, result): ...
The DBC class decorator does something like
def DBC(cls): def wrapper(*args, **kw): fn = cls() fn.args = args fn.kw = kw for pre in fn.__preconditions__: pre() result = fn(*args, **kw) for post in fn.__postconditions__: post(result) return wrapper
Pre and post conditions can access the args via self.args and self.kw. The method decorators would let you have multiple pre- and post-conditions. Or you could use "magic" names and omit the decorators.
I'd rather use magic names - something like:
@DBC class myfunction: def body(self, args): ... def requires(self): ... def ensures(self, result): ...
and then the DBC decorator can create a __call__ method. This still has one nasty problem though: the requires and ensures functions can't see function arguments. You could get around this by duplicating the argument list onto the other two, but who wants to do that?
You could do this pretty easily with a macro that returns (the AST for) something like this: def myfunction([func.body.params]): [func.requires.body] try: return_to_raise([func.body.body]) except Return as r: result, exc = r.args(0), None [func.ensures.body] return result except Exception as exc: [func.ensures.body] raise (I deliberately didn't write this in MacroPy style, but obviously if you really wanted to implement this, that's how you'd do it.) There are still a few things missing here. For example, many postconditions are specified in terms of the pre- and post- values of mutable parameters, with self as a very important special case. And fitting class invariant testing into this scheme should be extra fun. But I think it's all doable.