[Python-ideas] Re: Syntax for loop invariants

March 18, 2020

      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
...
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 
<mailto:steve@pearwood.info>> wrote:
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?*
> 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.
An actual real-world example would be more convincing.
> I propose the new syntax:
     >
     >     while running_condition(...):
     >         invariant invariant_condition(...)
     >
     >
     > The keyword 'invariant' is allowed only inside a loop.
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
    _______________________________________________
    Python-ideas mailing list -- python-ideas@python.org
    <mailto:python-ideas@python.org>
    To unsubscribe send an email to python-ideas-leave@python.org
    <mailto:python-ideas-leave@python.org>
    https://mail.python.org/mailman3/lists/python-ideas.python.org/
    Message archived at
    https://mail.python.org/archives/list/python-ideas@python.org/message/SJ7PHT...
    Code of Conduct: http://python.org/psf/codeofconduct/
_______________________________________________
Python-ideas mailing list -- python-ideas@python.org
To unsubscribe send an email to python-ideas-leave@python.org
https://mail.python.org/mailman3/lists/python-ideas.python.org/
Message archived at https://mail.python.org/archives/list/python-ideas@python.org/message/63R3II...
Code of Conduct: http://python.org/psf/codeofconduct/