Feature Request: Support for sequencing?

[sam-falvo]

TL;DR: Possible feature request.

Thank you for writing this module. For the first time, I've finally hit on a DbC library that covers 99% of my use-cases for the tool. It's easy to use and works really well! But, I have a question concerning that other 1%. I don't often need it, but when I do, I need it badly.

One of the nicer features of Eiffel's DbC support is the ability to reference "previous" versions of object fields. For instance, given:

class Counter(object):
    def __init__(self):
        self.ctr = 0
    def foo(self):
        xyz = arbitrary_function(self.ctr)
        self.ctr = self.ctr + 1
        return xyz

It'd be nice to be able to express the following (note: this is just pseudocode):

@ensure("...", lambda args, res: args.self.ctr == 1 + PREVIOUS(args.self.ctr))

Obviously, Python won't support the infrastructure by which that can happen, but if I'm allowed some chance to capture the old version of a member prior to the execution of the ensure assertion, I should be able to fake it by referencing that cached value at that time.

(Hopefully this makes sense. Apologies if I'm not making sense.)

I guess I can always split foo into two functions:

def foo(self):
    return self.internal_foo()[0]

@ensure("...", lambda args, res: res[1] + 1 == args.self.ctr)
def foo(self):
    ctr = self.ctr
    xyz = arbitrary_function(ctr)
    self.ctr = ctr + 1
    return (xyz, ctr)

However, this runs the risk of being verbose (two methods defined instead of one) and onerous (if many members need to be checked for sequential relationships).

Is there some other best-practice work-around for this particular use-case that I'm missing? Thanks!

[deadpixi]

Hi @sam-falvo

Please look at the preserve decorator that was just added. I think it might do what you're looking for.

The example problem you had above would look like this:

class Counter(object):
    def __init__(self):
        self.ctr = 0

    @preserve(lambda args: {"ctr": args.self.ctr})
    @ensure("counter was incremented by 1",
            lambda args, result, old: args.self.ctr == old.ctr + 1)
    def foo(self):
        self.ctr += 1

Please let me know if that works for you.

[sam-falvo]

That is exactly what I needed! Thank you!