Python has more and more optional tools for formal correctness cheking. Why not loop invariants? Loop invariant is such a statement that if it was true before the loop iteration, it will also be true after the iteration. It can be implemented as an assertion of an implication. now_value = False while running_condition(...): prev_value = now_value now_value = invariant_condition(...) assert now_value if prev_value else True Here for ellipsis we can substitute any values and variables. I propose the new syntax: while running_condition(...): invariant invariant_condition(...) The keyword 'invariant' is allowed only inside a loop. The interpreter will create a separate boolean variable holding the truth value of each invariant. On the loop entry, the value is reset to false. When the 'invariant' statement is encountered, the interpreter will evaluate the expression, test the implication 'prev_value -> now_value' and update the value. If the implication is not met, an exception will be thrown 'InvariantError' which is a subclass of 'AssertionError'. Like assertions, invariants will be checked only in debug mode. I am developing a library for formal proofs and such a feature would be handy. haael
On Tue, Mar 17, 2020 at 06:12:56PM +0000, haael wrote:
Python has more and more optional tools for formal correctness cheking.
Are you talking about third-party applications?
Why not loop invariants?
Wrong question :-) Adding new language features to Python isn't "default allow", adding every new feature that somebody suggests unless there is a reason not to add it. It is "default deny" -- new features have to be justified before they will be added, and even if they are justified, they still might not be added if: - the costs of the new feature outweigh the benefit; - there is sufficient opposition and insufficient support; - or nobody is interested enough to do the work. So the better question is: *Why add loop invariants as a language feature requiring a new keyword?*
An actual real-world example would be more convincing.
There are other kinds of invariants than just loop invariants. Can you justify why loop invariants are more important than other invariants? Can you point to other languages that offer loop invariants, but not other invariants or contracts such as preconditions and postconditions? For comparisons sake, this is how Eiffel handles loop invariants: https://www.eiffel.org/doc/eiffel/ET-_Instructions#Loop_invariants_and_varia... -- Steven
I'd have to agree with Steven here, I'm -0 on the proposal since it's not convincing (at least at the moment). haael wrote:
Python has more and more optional tools for formal correctness cheking. Why not loop invariants?
A better question would be "why add loop invariants?" rather than "why not add loop invariants?". The OP provides the basic syntax and a simple overview of how it would work, but doesn't provide any convincing arguments or real-world examples of why the feature should be added in the first place. That bar is already quite high for any new feature, but it's even higher for a new keyword for the language. I'd recommend finding some existing code and demonstrating how it could be significantly improved with the new feature. Concrete "before-and-after" examples can go a long way in making a strong argument for a feature proposal.
I am developing a library for formal proofs and such a feature would be handy.
This point could be worth further elaborating on: 1) Specifically, how would this feature help your library? 2) Could it similarly benefit other libraries? 3) How much does this benefit from being implemented at the language level? On Tue, Mar 17, 2020 at 11:00 PM Steven D'Aprano <steve@pearwood.info> wrote:
I am making a library that is able to prove that a function (without side effects) is correct for every input, without explicitly calling it on every input. It's quite similar to what Klee does to LLVM programs. https://klee.github.io/ Klee (and my solution too) works by unrolling loops. That means it can handle only functions whose loops are bound. Now, I noticed that in Python it is possible to test recursive functions with use of decorators. Let's say we have the function: def seq(n): if n == 0: return 0 else: return seq(n - 1) + 1 We have a condition: def cond(n): assert seq(n) == n * (n + 1) // 2 We want to prove it for every nonnegative integer. for_all(cond) My tool could do that if not the unbounded loop, implemented here in form of recursion. But Python has decorators. We can decorate the `seq` function or even capture it explicitly. I can make a special modified version of the function that returns a special symbolic variable. cutoff_n = 0 def cutoff(old_fn): def new_fn(n): if n < cutoff_n: return SymbolicVariable('seq_prev') else: return old_fn(n) @cutoff def seq(n): if n == 0: return 0 else: return seq(n - 1) + 1 Now I can perform an inductive proof. First, the case for n = 0. cutoff_n = 0 cond(0) Then, the induction step. n = SymbolicVariable('n') cutoff_n = SymbolicVariable('cutoff_n') assume(cutoff_n > 0) # add an assumption to the theory assume(n == cutoff_n + 1) # add an assumption to the theory r = seq(n) # `r` will be `SymbolicVariable('seq_prev') + 1` seq_prev = SymbolicVariable('seq_prev') assume(seq_prev == (n - 1) * n // 2) prove(r = n * (n + 1) // 2) This way it is possible to prove correctness of the recursive function. This was only possible because I had a hook. Decorators allow to inject some code to execute right where I needed. @decorator def recursive_function(x): ... recursive_function(f(x)) ... means: def recursive_function(x): ... something_before recursive_function(f(x)) something_after ... This is a very powerful tool to control the execution of a loop implemented in form of recursion. Now I want a similar feature to control execution of a normal `for` and `while` loop. With `for` it is possible thanks to iterators. for i in something: d += do_it(i) invariant something(d, i) I can do something like: for i in tweak(something): d += do_it(i) invariant something(d, i) Basically I can make an iterator that will run the loop only 2 times on symbollic variables. This is enough to prove any loop invariants inside. With `while' loops I need to tweak the running condition: while tweak(condition): d = modify(d) invariant something(d) The only missing feature is the ability to write invariants. I Python had it, it would be possible to write programs with in-line proofs in forms of assertions, type hints and invariants. What is bugging me is the assymetry: there is a nice way to hint functions, but there is none to hint loops. haael
On Mar 18, 2020, at 04:22, haael <haael@interia.pl> wrote:
What is bugging me is the assymetry: there is a nice way to hint functions, but there is none to hint loops.
Then Steve’s suggestion of a context manager seems perfect. It allows you to hint any statement, including a loop statement, by adding whatever code you want that gets run before and after the statement.
Yes https://docs.python.org/3/library/contextlib.html#contextlib.ContextDecorato... On Thu, Mar 19, 2020 at 3:26 PM Stephen J. Turnbull < turnbull.stephen.fw@u.tsukuba.ac.jp> wrote:
On Mar 19, 2020, at 06:23, Stephen J. Turnbull <turnbull.stephen.fw@u.tsukuba.ac.jp> wrote:
Well, it only goes so far. A decorator is a call to a decorator function: a with statement is construction, entering, and exiting a context manager object. A decorator function is called once, when the function it decorates is defined; a context manager is called every time the statement it manages executes. A decorator function takes the decorated function as its parameter, and the wrapper function it returns gets to see the function’s arguments and its return value; a context manager has no access to the suite it manages or any of the variables it works on. And I think the last one is particularly important here. If you’re thinking of verifying some code by checking that the output bears some relation to the input, a decorator has an obvious place to do that; with a context manager, it’s not even clear what the “input” and “output” of a suite are, but however you define them, you don’t have access to them (barring some tricks you can do with ugly frame hacks). But still, despite the differences, there are some parallels. In particular, if you’re looking to “tag” some code with additional information, decorators and with statements can do that in similar enough ways. Where I think your analogy might be really useful is evaluating the periodic proposals to give context managers access to their managed code or namespace or whatever. Hopefully you or someone else remembers your post next time one of those threads starts. :)
On Wed, Mar 18, 2020 at 09:26:52PM -0700, Andrew Barnert via Python-ideas wrote:
Wasn't me, it was the other Stephen who spells his name with a "ph" :-) Context managers are great when the CM has its own standard behaviour that gets reused over and over again, like open files. You need to write the the context manager once, and you can use it over and over again. The only standard part of a loop invariant is, as far as I can tell, to save a copy of the loop variable at the start of the loop. Everything else is likely to be unique. So each loop will need its own context manager, meaning its own class. The *actual* invariant will be buried far away, in a CM class, rather than right there next to the loop. You might be able to reuse some invariant CMs by generalising the invariants into a meta-invariant, but I expect that to lead to over- abstract code that is unclear and hard to follow. But in general, each loop will need its own CM class. Because the actual invariant is far away, buried in a class rather than there next to the loop, we will rely on a unique, descriptive name for every loop that has an invariant. Naming is hard: that's not going to work well, and we'll end up with multiple context managers with generic names like "invariant1", "invariant2" etc. Worse: the condition will likely need to be written as a string, or a lambda, in order to delay evaluation. In Eiffel, invariants are a block. Forcing invariants into a context manager would have all the disadvantages of forcing every for loop into a call to map() with a named function. I don't think the context manager idea will be practical unless you have only a very small number of very similar, simple, invariants. -- Steve
Steven D'Aprano writes:
Wasn't me, it was the other Stephen who spells his name with a "ph" :-)
Guilty as charged, on both counts.
I see no reason why that will be true for many invariants. The context manager class would be simple, in principle: __entry__, __exit__, and invariants. The expression in the with statement would be a constructor.
Worse: the condition will likely need to be written as a string, or a lambda, in order to delay evaluation.
Or a local def. This is correct, as far as I know. I would expect the example from Wikipedia (https://en.wikipedia.org/wiki/Loop_invariant#Informal_example) translated to Python would be written in the "condition as string" implementation as def max(n, a): m = a[0] # m equals the maximum value in a[0...0] i = 1 while (i != n) { with Invariants('m == max(a[0:i])'): # m equals the maximum value in a[0...i-1] if (m < a[i]): m = a[i] # m equals the maximum value in a[0...i] i += 1 # m equals the maximum value in a[0...i-1] # m equals the maximum value in a[0...i-1], and i==n return m So that's a little bit ugly because the condition is a string. The real problem I see is getting access to the bindings, which is likely to involve passing in globals() and locals() to the constructor, which isn't nice but also not so bad: Invariants(globals(), locals(), 'm = max(a[0:i])', # add more invariants here if you like ) Unfortunately, locals() is not guaranteed by the language to update with changes to the locals (although it appears to in CPython 3.8.2).
In Eiffel, invariants are a block.
In Python, I suspect you would want each invariant to be a suite, since the calculations you can do with expressions are limited, and you wouldn't want to define a function for the reasons of locality to the loop that you mentioned already.
I really doubt it. I think some complex invariants would need to be implemented as named functions, but much of the time all of the invariants could be inlined, and almost all of the time most of the invariants could be inlined.
I don't think the context manager idea will be practical unless you have only a very small number of very similar, simple, invariants.
I agree, but I also think that generalizes to the whole idea of invariants in Python. I don't think programming with invariants is likely to be Python's strong suit. I'd loved to be proved wrong (not that I'd use them myself that I can see, but I know others have explored the idea of automatically verifying invariants and it would be cool!) If so, I'd be supportive of a syntax change. Steve
On 21Mar2020 12:15, Stephen J. Turnbull <turnbull.stephen.fw@u.tsukuba.ac.jp> wrote:
Twio things: 1: Might I point out to everyone the icontract PyPI module (maybe I've missing this in the discussion?), which does all this kind of thing for functions (programming by contract, thus the function level focus). The important point here is that it uses lambda to express the assertions: @require(lambda foo: foo > 1) def func(foo): ... There's a post condition decorator, and invariants etc. It does funky function signature inspection to match up the lambda parameter names to the function paraemeter names. very cool. 2: Anyway, a salient point here is that you can write _arbitrary_ invariants as context managers using closures to get the locals/globals stuff (icontract isn't doing this, but it is heavy on the lambdas). For example, maybe: from ... import invariant_cm def max(n, a): m = a[0] # m equals the maximum value in a[0...0] i = 1 while (i != n) { with invariant_cm(lambda: m == max(a[0:i])): where invariant_cm came out of your library for checking before and after the suite. The closure gets you the locals/globals directly without cumbersomeness. Cheers, Cameron Simpson <cs@cskk.id.au>
haael writes:
Can you do this with a context manager? The syntax would be now_values = None while running_condition(...): with invariant_conditions(now_values, invariant1, ...): # loop body goes here The idea is that the __enter__ of the invariant_conditions context manager would initialize 'now_values' to [False] * invariants_count if now_values == None. The __exit__ would loop over zip(now_values, invariants), doing prev_value = now_value now_value = invariant(...) assert now_value if prev_value else True for each. An alternative definition of loop invariant from Wikipedia (https://en.wikipedia.org/wiki/Loop_invariant) suggest the simpler syntax (and implementation) while running_condition(...): with invariant_conditions(invariant1, ...): # loop body goes here where the invariants are simply asserted in __enter__, stored in an attribute of the context manager object, and asserted again in __exit__. In both cases, the evaluations would be controlled by a global variable, which would have minimal performance impact. You may also want to look at MacroPy, which allows you to implement syntax like you've proposed. Steve
On Tue, Mar 17, 2020 at 06:12:56PM +0000, haael wrote:
Python has more and more optional tools for formal correctness cheking.
Are you talking about third-party applications?
Why not loop invariants?
Wrong question :-) Adding new language features to Python isn't "default allow", adding every new feature that somebody suggests unless there is a reason not to add it. It is "default deny" -- new features have to be justified before they will be added, and even if they are justified, they still might not be added if: - the costs of the new feature outweigh the benefit; - there is sufficient opposition and insufficient support; - or nobody is interested enough to do the work. So the better question is: *Why add loop invariants as a language feature requiring a new keyword?*
An actual real-world example would be more convincing.
There are other kinds of invariants than just loop invariants. Can you justify why loop invariants are more important than other invariants? Can you point to other languages that offer loop invariants, but not other invariants or contracts such as preconditions and postconditions? For comparisons sake, this is how Eiffel handles loop invariants: https://www.eiffel.org/doc/eiffel/ET-_Instructions#Loop_invariants_and_varia... -- Steven
I'd have to agree with Steven here, I'm -0 on the proposal since it's not convincing (at least at the moment). haael wrote:
Python has more and more optional tools for formal correctness cheking. Why not loop invariants?
A better question would be "why add loop invariants?" rather than "why not add loop invariants?". The OP provides the basic syntax and a simple overview of how it would work, but doesn't provide any convincing arguments or real-world examples of why the feature should be added in the first place. That bar is already quite high for any new feature, but it's even higher for a new keyword for the language. I'd recommend finding some existing code and demonstrating how it could be significantly improved with the new feature. Concrete "before-and-after" examples can go a long way in making a strong argument for a feature proposal.
I am developing a library for formal proofs and such a feature would be handy.
This point could be worth further elaborating on: 1) Specifically, how would this feature help your library? 2) Could it similarly benefit other libraries? 3) How much does this benefit from being implemented at the language level? On Tue, Mar 17, 2020 at 11:00 PM Steven D'Aprano <steve@pearwood.info> wrote:
I am making a library that is able to prove that a function (without side effects) is correct for every input, without explicitly calling it on every input. It's quite similar to what Klee does to LLVM programs. https://klee.github.io/ Klee (and my solution too) works by unrolling loops. That means it can handle only functions whose loops are bound. Now, I noticed that in Python it is possible to test recursive functions with use of decorators. Let's say we have the function: def seq(n): if n == 0: return 0 else: return seq(n - 1) + 1 We have a condition: def cond(n): assert seq(n) == n * (n + 1) // 2 We want to prove it for every nonnegative integer. for_all(cond) My tool could do that if not the unbounded loop, implemented here in form of recursion. But Python has decorators. We can decorate the `seq` function or even capture it explicitly. I can make a special modified version of the function that returns a special symbolic variable. cutoff_n = 0 def cutoff(old_fn): def new_fn(n): if n < cutoff_n: return SymbolicVariable('seq_prev') else: return old_fn(n) @cutoff def seq(n): if n == 0: return 0 else: return seq(n - 1) + 1 Now I can perform an inductive proof. First, the case for n = 0. cutoff_n = 0 cond(0) Then, the induction step. n = SymbolicVariable('n') cutoff_n = SymbolicVariable('cutoff_n') assume(cutoff_n > 0) # add an assumption to the theory assume(n == cutoff_n + 1) # add an assumption to the theory r = seq(n) # `r` will be `SymbolicVariable('seq_prev') + 1` seq_prev = SymbolicVariable('seq_prev') assume(seq_prev == (n - 1) * n // 2) prove(r = n * (n + 1) // 2) This way it is possible to prove correctness of the recursive function. This was only possible because I had a hook. Decorators allow to inject some code to execute right where I needed. @decorator def recursive_function(x): ... recursive_function(f(x)) ... means: def recursive_function(x): ... something_before recursive_function(f(x)) something_after ... This is a very powerful tool to control the execution of a loop implemented in form of recursion. Now I want a similar feature to control execution of a normal `for` and `while` loop. With `for` it is possible thanks to iterators. for i in something: d += do_it(i) invariant something(d, i) I can do something like: for i in tweak(something): d += do_it(i) invariant something(d, i) Basically I can make an iterator that will run the loop only 2 times on symbollic variables. This is enough to prove any loop invariants inside. With `while' loops I need to tweak the running condition: while tweak(condition): d = modify(d) invariant something(d) The only missing feature is the ability to write invariants. I Python had it, it would be possible to write programs with in-line proofs in forms of assertions, type hints and invariants. What is bugging me is the assymetry: there is a nice way to hint functions, but there is none to hint loops. haael
On Mar 18, 2020, at 04:22, haael <haael@interia.pl> wrote:
What is bugging me is the assymetry: there is a nice way to hint functions, but there is none to hint loops.
Then Steve’s suggestion of a context manager seems perfect. It allows you to hint any statement, including a loop statement, by adding whatever code you want that gets run before and after the statement.
Yes https://docs.python.org/3/library/contextlib.html#contextlib.ContextDecorato... On Thu, Mar 19, 2020 at 3:26 PM Stephen J. Turnbull < turnbull.stephen.fw@u.tsukuba.ac.jp> wrote:
On Mar 19, 2020, at 06:23, Stephen J. Turnbull <turnbull.stephen.fw@u.tsukuba.ac.jp> wrote:
Well, it only goes so far. A decorator is a call to a decorator function: a with statement is construction, entering, and exiting a context manager object. A decorator function is called once, when the function it decorates is defined; a context manager is called every time the statement it manages executes. A decorator function takes the decorated function as its parameter, and the wrapper function it returns gets to see the function’s arguments and its return value; a context manager has no access to the suite it manages or any of the variables it works on. And I think the last one is particularly important here. If you’re thinking of verifying some code by checking that the output bears some relation to the input, a decorator has an obvious place to do that; with a context manager, it’s not even clear what the “input” and “output” of a suite are, but however you define them, you don’t have access to them (barring some tricks you can do with ugly frame hacks). But still, despite the differences, there are some parallels. In particular, if you’re looking to “tag” some code with additional information, decorators and with statements can do that in similar enough ways. Where I think your analogy might be really useful is evaluating the periodic proposals to give context managers access to their managed code or namespace or whatever. Hopefully you or someone else remembers your post next time one of those threads starts. :)
On Wed, Mar 18, 2020 at 09:26:52PM -0700, Andrew Barnert via Python-ideas wrote:
Wasn't me, it was the other Stephen who spells his name with a "ph" :-) Context managers are great when the CM has its own standard behaviour that gets reused over and over again, like open files. You need to write the the context manager once, and you can use it over and over again. The only standard part of a loop invariant is, as far as I can tell, to save a copy of the loop variable at the start of the loop. Everything else is likely to be unique. So each loop will need its own context manager, meaning its own class. The *actual* invariant will be buried far away, in a CM class, rather than right there next to the loop. You might be able to reuse some invariant CMs by generalising the invariants into a meta-invariant, but I expect that to lead to over- abstract code that is unclear and hard to follow. But in general, each loop will need its own CM class. Because the actual invariant is far away, buried in a class rather than there next to the loop, we will rely on a unique, descriptive name for every loop that has an invariant. Naming is hard: that's not going to work well, and we'll end up with multiple context managers with generic names like "invariant1", "invariant2" etc. Worse: the condition will likely need to be written as a string, or a lambda, in order to delay evaluation. In Eiffel, invariants are a block. Forcing invariants into a context manager would have all the disadvantages of forcing every for loop into a call to map() with a named function. I don't think the context manager idea will be practical unless you have only a very small number of very similar, simple, invariants. -- Steve
Steven D'Aprano writes:
Wasn't me, it was the other Stephen who spells his name with a "ph" :-)
Guilty as charged, on both counts.
I see no reason why that will be true for many invariants. The context manager class would be simple, in principle: __entry__, __exit__, and invariants. The expression in the with statement would be a constructor.
Worse: the condition will likely need to be written as a string, or a lambda, in order to delay evaluation.
Or a local def. This is correct, as far as I know. I would expect the example from Wikipedia (https://en.wikipedia.org/wiki/Loop_invariant#Informal_example) translated to Python would be written in the "condition as string" implementation as def max(n, a): m = a[0] # m equals the maximum value in a[0...0] i = 1 while (i != n) { with Invariants('m == max(a[0:i])'): # m equals the maximum value in a[0...i-1] if (m < a[i]): m = a[i] # m equals the maximum value in a[0...i] i += 1 # m equals the maximum value in a[0...i-1] # m equals the maximum value in a[0...i-1], and i==n return m So that's a little bit ugly because the condition is a string. The real problem I see is getting access to the bindings, which is likely to involve passing in globals() and locals() to the constructor, which isn't nice but also not so bad: Invariants(globals(), locals(), 'm = max(a[0:i])', # add more invariants here if you like ) Unfortunately, locals() is not guaranteed by the language to update with changes to the locals (although it appears to in CPython 3.8.2).
In Eiffel, invariants are a block.
In Python, I suspect you would want each invariant to be a suite, since the calculations you can do with expressions are limited, and you wouldn't want to define a function for the reasons of locality to the loop that you mentioned already.
I really doubt it. I think some complex invariants would need to be implemented as named functions, but much of the time all of the invariants could be inlined, and almost all of the time most of the invariants could be inlined.
I don't think the context manager idea will be practical unless you have only a very small number of very similar, simple, invariants.
I agree, but I also think that generalizes to the whole idea of invariants in Python. I don't think programming with invariants is likely to be Python's strong suit. I'd loved to be proved wrong (not that I'd use them myself that I can see, but I know others have explored the idea of automatically verifying invariants and it would be cool!) If so, I'd be supportive of a syntax change. Steve
On 21Mar2020 12:15, Stephen J. Turnbull <turnbull.stephen.fw@u.tsukuba.ac.jp> wrote:
Twio things: 1: Might I point out to everyone the icontract PyPI module (maybe I've missing this in the discussion?), which does all this kind of thing for functions (programming by contract, thus the function level focus). The important point here is that it uses lambda to express the assertions: @require(lambda foo: foo > 1) def func(foo): ... There's a post condition decorator, and invariants etc. It does funky function signature inspection to match up the lambda parameter names to the function paraemeter names. very cool. 2: Anyway, a salient point here is that you can write _arbitrary_ invariants as context managers using closures to get the locals/globals stuff (icontract isn't doing this, but it is heavy on the lambdas). For example, maybe: from ... import invariant_cm def max(n, a): m = a[0] # m equals the maximum value in a[0...0] i = 1 while (i != n) { with invariant_cm(lambda: m == max(a[0:i])): where invariant_cm came out of your library for checking before and after the suite. The closure gets you the locals/globals directly without cumbersomeness. Cheers, Cameron Simpson <cs@cskk.id.au>
haael writes:
Can you do this with a context manager? The syntax would be now_values = None while running_condition(...): with invariant_conditions(now_values, invariant1, ...): # loop body goes here The idea is that the __enter__ of the invariant_conditions context manager would initialize 'now_values' to [False] * invariants_count if now_values == None. The __exit__ would loop over zip(now_values, invariants), doing prev_value = now_value now_value = invariant(...) assert now_value if prev_value else True for each. An alternative definition of loop invariant from Wikipedia (https://en.wikipedia.org/wiki/Loop_invariant) suggest the simpler syntax (and implementation) while running_condition(...): with invariant_conditions(invariant1, ...): # loop body goes here where the invariants are simply asserted in __enter__, stored in an attribute of the context manager object, and asserted again in __exit__. In both cases, the evaluations would be controlled by a global variable, which would have minimal performance impact. You may also want to look at MacroPy, which allows you to implement syntax like you've proposed. Steve
participants (8)
-
Alex Hall -
Andrew Barnert -
Cameron Simpson -
haael -
Kyle Stanley -
Stephen J. Turnbull -
Steve Jorgensen -
Steven D'Aprano