[Python-ideas] "old" values in postconditions

[James Lu]

You could disassemble (import dis) the lambda to biew the names of the lambdas.

@before(lambda self, key, _, length, get: self.length(), self.get(key))

Perhaps you could disassemble the function code and look at all operations or accesses that are done to “old.” and evaluate those expressions before the function runs. Then you could “replace” the expression.
@post(lambda self, key, old: old.get is None and old.length + 1 ==
self.length())

Either the system would grab old.get and old.length or be greedy and grab old.get is None and old.length + 1. It would then replace the old.get and old.length with injects that only respond to is None and +1.

Or, a syntax like this 
@post(lambda self, key, old: [old.get(old.key)] is None and [old.self.length() + 1] ==
self.length())

Where the stuff inside the brackets is evaluated before the decorated function runs. It would be useful for networking functions or functions that do something ephemeral, where data related to the value being accessed needed for the expression no longer exists after the function. 

This does conflict with list syntax forever, so maybe either force people to do list((expr,)) or use an alternate syntax like one item set syntax { } or double set syntax {{ }} or double list syntax [[ ]]. Ditto with having to avoid the literals for the normal meaning.

You could modify Python to accept any expression for the lambda function and propose that as a PEP. (Right now it’s hardcoded as a dotted name and optionally a single argument list surrounded by parentheses.)

I suggest that instead of “@before” it’s “@snapshot” and instead of “old” it’s “snapshot”.

Python does have unary plus/minus syntax as well as stream operators (<<, >>) and list slicing syntax and the @ operator and operators & and | if you want to play with syntax. There’s also the line continuation character for crazy lambdas.

Personally I prefer
@post(lambda self, key, old: {{old.self.get(old.key)}} and {{old.self.length() + 1}} ==
self.length())

because it’s explicit about what it does (evaluate the expressions within {{ }} before the function runs. I also find it elegant.

Alternatively, inside the {{ }} could be a special scope where locals() is all the arguments @pre could’ve received as a dictionary. For either option you can remove the old parameter from the lambda. Example:
@post(lambda self, key: {{self.get(key)}} and {{self.length() + 1}} ==
self.length())

Perhaps the convention should be to write {{ expr }} (with the spaces in between).

You’d probably have to use the ast module to inspect it instead of the dis modul. Then find some way to reconstruct the expressions inside the double brackets- perhaps by reconstructing the AST and compiling it to a code object, or perhaps by finding the part of the string the expression is located. dis can give you the code as a string and you can run a carefully crafted regex on it.