return in loop for ?

[Duncan Booth]

Re: return in loop for ?

Steven D'Aprano wrote:
[color=blue][color=green]
>> While outwardly they apear to offer a technique for making software
>> more reliable there are two shortcomings I'm leery of. First, no
>> verification program can verify itself;[/color]
>
> That's not a problem if there exists a verification program A which
> can't verify itself but can verify program B, which in turn also can't
> verify itself but will verify program A.
>[/color]
That is logically equivalent to the first case, so it doesn't get you
anywhere. (Just combine A and B into a single program which invokes A
unless the input is A when it invokes B instead.)

[Peter Hansen]

Re: return in loop for ?

Duncan Booth wrote:[color=blue]
> In practice it is impossible to write code in Python (or most
> languages) with only one return point from a function: any line could throw
> an exception which is effectively another return point, so the cleanup has
> to be done properly anyway.[/color]

def funcWithGuarant eedOneExitPoint ():
try:
# do some stuff, or
pass
finally:
return None

Of course, you might have mistyped something (e.g. "none") and still
manage to get an exception, but at least in the above example it's still
only a single exit point, even if not the one you thought it was. ;-)

-Peter

[Peter Hansen]

Re: return in loop for ?

Fredrik Lundh wrote:[color=blue]
> Steve Holden wrote:
>[color=green]
>>sepcification s[/color]
>
> did you mean: sceptifications ?
>
> (otoh, with 11,100 google hits, "sepcifications " should probably be
> considered as a fully acceptable alternate spelling ;-)[/color]

Not if they're all in pages at site:holdenweb. com ! <grin>

[Scott David Daniels]

Re: return in loop for ?

Fredrik Lundh wrote:[color=blue]
> Steve Holden wrote:[color=green]
>>sepcification s[/color]
> did you mean: sceptifications ?[/color]
QOTW!

I love it. I need to insert this in my vocabulary instantly!

--Scott David Daniels
scott.daniels@a cm.org

[Roy Smith]

Re: return in loop for ?

"bonono@gmail.c om" <bonono@gmail.c om> wrote:[color=blue]
> Interestingly, I just saw a thread over at TurboGears(or is it this
> group, I forgot) about this multiple return issue and there are people
> who religiously believe that a function can have only one exit point.
>
> def f():
> r = None
> for i in range(20):
> if i > 10:
> r = 10
> break
> if r is None: something
> else: return r[/color]

"Single entrance, single exit" is a philosophy (religion?) that's been
around for a while. The basic thought is that every code block should have
a single entrance and a single exit.

Back in the dark old days of gotos, there was a lot of spaghetti code
written with gotos jumping all over the place, even in and out of the
middle of loops. Then, in 1968, Dijkstra wrote his famous "Go To Statement
Considered Harmful" (http://www.acm.org/classics/oct95/) which spawned the
whole structured programming concept, and SESE is the logical outgrowth of
that.

The problem with SESE is that if you follow it strictly, you end up with
things like the example given above where you have to invent some temporary
variable, and an extra test at the end of the loop. The cure is worse than
the disease.

In any case, in a language which has exceptions, it's almost impossible to
really have true SESE, since an exception could be thrown from almost
anywhere. To be fair, there are those who use this to argue that
exceptions themselves are a bad thing. In my last job, the official style
guide said to not use exceptions in C++ because they generate confusing
flow of control, but I think that's becomming the minority view these days.

[Mike Meyer]

Re: return in loop for ?

Duncan Booth <duncan.booth@i nvalid.invalid> writes:[color=blue]
> In practice it is impossible to write code in Python (or most
> languages) with only one return point from a function: any line could throw
> an exception which is effectively another return point, so the cleanup has
> to be done properly anyway.[/color]

This simply isn't true. Not having a return statement is no worse than
not having a goto. Well, maybe it's a little worse. A number of
languages don't have it. Rewriting my example to have a single return
is easy:

def f():
for i in range(20):
if i > 10: break
inloop() # Added for a later example
return

This isn't noticably different than the original. Of course, if you
want to *do* something after the for loop, you have to test
the conditional again (or use a flag variable):

def f():
for i in range(20):
if i > 10: break
inloop()
if not (i > 10):
afterloop()
return

In my experience, people who believe that single exit is a good
principle often believe that's true at the statement level as well, so
that "break" and "continue" in for loops are bad things. That means
you have to rewrite the above as:

def f():
for i in [j for j in range(20) if j <= 10]:
inloop()
if not (i > 10):
afterloop()
return

At this point, the argument collapses in a cloud of impracticality,
and we go back to returning from wherever we want to.

<mike
--
Mike Meyer <mwm@mired.or g> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Mike Meyer]

Re: return in loop for ?

Roy Smith <roy@panix.co m> writes:[color=blue]
> In any case, in a language which has exceptions, it's almost impossible to
> really have true SESE, since an exception could be thrown from almost
> anywhere. To be fair, there are those who use this to argue that
> exceptions themselves are a bad thing. In my last job, the official style
> guide said to not use exceptions in C++ because they generate confusing
> flow of control, but I think that's becomming the minority view these days.[/color]

I really like Eiffel's model of exception handling. Instead of having
the ability to catch exceptions at arbitrary points in your code -
which, as you point out - can lead to confusing flow of control - a
function can have an exception handler - a "retry" clause - that
handles all exceptions in that function. Further, the retry clause
does one of two things: it either starts the function over again, or
passes the exception back up the chain. I'm not sure that it stacks up
on the practicality scale, but it certainly leads to a more
comprehensible program when you are dealing with lots of exceptions.

<mike
--
Mike Meyer <mwm@mired.or g> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Magnus Lycka]

Re: return in loop for ?

Mike Meyer wrote:[color=blue]
> This isn't noticably different than the original. Of course, if you
> want to *do* something after the for loop, you have to test
> the conditional again (or use a flag variable):
>
> def f():
> for i in range(20):
> if i > 10: break
> inloop()
> if not (i > 10):
> afterloop()
> return[/color]

Nope. Use for-else, like this:

def f():
for i in range(20):
if i > 10: break
inloop()
else:
afterloop()
return


In practice, a good reason to follow Knuth rather than Dijkstra,
and allow multiple exits, is that the more levels of indentation
we have, the more difficult it is to follow the code.

Flat is better than nested...

With multiple exits, we can typically often avoid nested else
blocks etc, and get a much more linear program flow, where
error cases etc lead to a premature exits, and the normal,
full flow just runs straight from top to bottom in a function.

[Steven D'Aprano]

Re: return in loop for ?

On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:
[color=blue]
> Steven D'Aprano wrote:
>[color=green][color=darkred]
>>> While outwardly they apear to offer a technique for making software
>>> more reliable there are two shortcomings I'm leery of. First, no
>>> verification program can verify itself;[/color]
>>
>> That's not a problem if there exists a verification program A which
>> can't verify itself but can verify program B, which in turn also can't
>> verify itself but will verify program A.
>>[/color]
> That is logically equivalent to the first case, so it doesn't get you
> anywhere. (Just combine A and B into a single program which invokes A
> unless the input is A when it invokes B instead.)[/color]

Then there you go, there is a single program which can verify itself.

I think you are confabulating the impossibility of any program which can
verify ALL programs (including itself) with the impossibility of a program
verifying itself. Programs which operate on their own source code do not
violate the Halting Problem. Neither do programs which verify some
subset of the set of all possibly programs.


--
Steven.

[Steve Holden]

Re: return in loop for ?

Steven D'Aprano wrote:[color=blue]
> On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:
>
>[color=green]
>>Steven D'Aprano wrote:
>>
>>[color=darkred]
>>>>While outwardly they apear to offer a technique for making software
>>>>more reliable there are two shortcomings I'm leery of. First, no
>>>>verificatio n program can verify itself;
>>>
>>>That's not a problem if there exists a verification program A which
>>>can't verify itself but can verify program B, which in turn also can't
>>>verify itself but will verify program A.
>>>[/color]
>>
>>That is logically equivalent to the first case, so it doesn't get you
>>anywhere. (Just combine A and B into a single program which invokes A
>>unless the input is A when it invokes B instead.)[/color]
>
>
> Then there you go, there is a single program which can verify itself.
>
> I think you are confabulating the impossibility of any program which can
> verify ALL programs (including itself) with the impossibility of a program
> verifying itself. Programs which operate on their own source code do not
> violate the Halting Problem. Neither do programs which verify some
> subset of the set of all possibly programs.
>
>[/color]
There seems to have been some misattribution in recent messages, since I
believe it was *me* who raised doubts about a program verifying itself.
This has nothing to do with the Halting Problem at all. A very simple
possible verification program is one that outputs True for any input.
This will also verify itself. Unfortunately its output will be invalid
in that and many other cases.

I maintain that we cannot rely on any program's assertions about its own
formal correctness.

regards
Steve
--
Steve Holden +44 150 684 7255 +1 800 494 3119
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Steve Holden]

Re: return in loop for ?

Steven D'Aprano wrote:[color=blue]
> On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:
>
>[color=green]
>>Steven D'Aprano wrote:
>>
>>[color=darkred]
>>>>While outwardly they apear to offer a technique for making software
>>>>more reliable there are two shortcomings I'm leery of. First, no
>>>>verificatio n program can verify itself;
>>>
>>>That's not a problem if there exists a verification program A which
>>>can't verify itself but can verify program B, which in turn also can't
>>>verify itself but will verify program A.
>>>[/color]
>>
>>That is logically equivalent to the first case, so it doesn't get you
>>anywhere. (Just combine A and B into a single program which invokes A
>>unless the input is A when it invokes B instead.)[/color]
>
>
> Then there you go, there is a single program which can verify itself.
>
> I think you are confabulating the impossibility of any program which can
> verify ALL programs (including itself) with the impossibility of a program
> verifying itself. Programs which operate on their own source code do not
> violate the Halting Problem. Neither do programs which verify some
> subset of the set of all possibly programs.
>
>[/color]
There seems to have been some misattribution in recent messages, since I
believe it was *me* who raised doubts about a program verifying itself.
This has nothing to do with the Halting Problem at all. A very simple
possible verification program is one that outputs True for any input.
This will also verify itself. Unfortunately its output will be invalid
in that and many other cases.

I maintain that we cannot rely on any program's assertions about its own
formal correctness.

regards
Steve
--
Steve Holden +44 150 684 7255 +1 800 494 3119
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Steven D'Aprano]

Re: return in loop for ?

On Fri, 25 Nov 2005 08:36:48 +0000, Steve Holden wrote:
[color=blue][color=green][color=darkred]
>>>>That's not a problem if there exists a verification program A which
>>>>can't verify itself but can verify program B, which in turn also can't
>>>>verify itself but will verify program A.
>>>>
>>>
>>>That is logically equivalent to the first case, so it doesn't get you
>>>anywhere. (Just combine A and B into a single program which invokes A
>>>unless the input is A when it invokes B instead.)[/color]
>>
>>
>> Then there you go, there is a single program which can verify itself.
>>
>> I think you are confabulating the impossibility of any program which can
>> verify ALL programs (including itself) with the impossibility of a program
>> verifying itself. Programs which operate on their own source code do not
>> violate the Halting Problem. Neither do programs which verify some
>> subset of the set of all possibly programs.
>>
>>[/color]
> There seems to have been some misattribution in recent messages, since I
> believe it was *me* who raised doubts about a program verifying itself.[/color]

Fair enough.
[color=blue]
> This has nothing to do with the Halting Problem at all.[/color]

On the contrary, the Halting Problem is just a sub-set of the verification
problem. Failure to halt when it is meant to is just one possible way a
program can fail verification.

On the one hand, the Halting Problem is much simpler than the question of
proving formal correctness, since you aren't concerned whether your
program actually does what you want it to do, so long as it halts.

But on the other hand, the Halting Problem is so much harder that it
actually becomes impossible -- it insists on a single algorithm which is
capable of checking every imaginable input.

Since real source code verifiers make no such sweeping claims to
perfection (or at least if they do they are wrong to do so), there is no
such proof that they are impossible. By using more and more elaborate
checking algorithms, your verifier gets better at correctly verifying
source code -- but there is no guarantee that it will be able to correctly
verify every imaginable program.

[color=blue]
> A very simple
> possible verification program is one that outputs True for any input.
> This will also verify itself. Unfortunately its output will be invalid
> in that and many other cases.[/color]

No doubt. But slightly more complex verification programs may actually
analyse the source code of some arbitrary program, attempt to use formal
algebra and logic to prove correctness, returning True or False as
appropriate.

That program itself may have been painstakingly proven correct by teams of
computer scientists, logicians and mathematicians, after which the
correctness of its results are as certain as any computer program can be.
That is the program we should be using, not your example.

[color=blue]
> I maintain that we cannot rely on any program's assertions about its own
> formal correctness.[/color]

There are two ways of understanding that statement.

If all you mean to say is "We cannot rely on any program's assertions
about any other programs formal correctness, including its own", then I
can't dispute that -- I don't know how well formal correctness checking
programs are. It is possibly, I suppose, that the state of the art merely
returns True regardless of the input, although I imagine a more realistic
estimate is that they would at least call something like pylint to check
for syntax errors, and return False if they find any.

But if you mean to say "While we can rely on the quality of correctness
checkers in general, but not when they run on their own source code" then
I think you are utterly mistaken to assume that there is some magic
quality of a verification program's own source code that prevents the
verification program working correctly on itself.

And that was my point: formal correctness checking programs will be as
good as testing themselves as they are at testing other programs. If you
trust them to check other programs, you have no reason not to trust them
to check themselves.



--
Steven.

[Steve Holden]

Re: return in loop for ?

Steven D'Aprano wrote:[color=blue]
> On Fri, 25 Nov 2005 08:36:48 +0000, Steve Holden wrote:[/color]
[...][color=blue]
>[color=green]
>>I maintain that we cannot rely on any program's assertions about its own
>>formal correctness.[/color]
>
>
> There are two ways of understanding that statement.
>
> If all you mean to say is "We cannot rely on any program's assertions
> about any other programs formal correctness, including its own", then I
> can't dispute that -- I don't know how well formal correctness checking
> programs are. It is possibly, I suppose, that the state of the art merely
> returns True regardless of the input, although I imagine a more realistic
> estimate is that they would at least call something like pylint to check
> for syntax errors, and return False if they find any.
>[/color]
No, I didn't mean to say that. Although of course there *are* issues
surrounding the semantic edge cases to do with implementation on real
hardware that do require formal theories to be limited and hedged with
restrictions due to the restrictions if the underlying hardware, for
example. Numerical analysts, though, have been well used to reasoning
about differences between the theoretical behaviour of algorithms and
the behaviour of their implementations for decades, so this is nothing new.
[color=blue]
> But if you mean to say "While we can rely on the quality of correctness
> checkers in general, but not when they run on their own source code" then
> I think you are utterly mistaken to assume that there is some magic
> quality of a verification program's own source code that prevents the
> verification program working correctly on itself.
>[/color]
Well naturally I can't stop you thinking that, so I won't try.
[color=blue]
> And that was my point: formal correctness checking programs will be as
> good as testing themselves as they are at testing other programs. If you
> trust them to check other programs, you have no reason not to trust them
> to check themselves.
>[/color]
Your bald assertion fails to change my mind about that, but it is quite
a fine theoretical issue. For what it's worth, I *have* discussed this
issue with academic formal proof specialists, some of whom have admitted
that it's a (theoretical) problem. But in the world of the practical I
wouldn't disagree with your characterisatio n of the state of the art.

regards
Steve
--
Steve Holden +44 150 684 7255 +1 800 494 3119
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Duncan Booth]

Re: return in loop for ?

Steven D'Aprano wrote:
[color=blue]
> Since real source code verifiers make no such sweeping claims to
> perfection (or at least if they do they are wrong to do so), there is
> no such proof that they are impossible. By using more and more
> elaborate checking algorithms, your verifier gets better at correctly
> verifying source code -- but there is no guarantee that it will be
> able to correctly verify every imaginable program.
>[/color]
I'm sure you can make a stronger statement than your last one. Doesn't
Godel's incompleteness theorem apply? I would have thought that no matter
how elaborate the checking it is guaranteed there exist programs which are
correct but your verifier cannot prove that they are.

[Sybren Stuvel]

Re: return in loop for ?

Duncan Booth enlightened us with:[color=blue]
> I would have thought that no matter how elaborate the checking it is
> guaranteed there exist programs which are correct but your verifier
> cannot prove that they are.[/color]

Yep, that's correct. I thought the argument was similar to the proof
that no program (read: Turing machine) can determine whether a program
will terminate or not.

Sybren
--
The problem with the world is stupidity. Not saying there should be a
capital punishment for stupidity, but why don't we just take the
safety labels off of everything and let the problem solve itself?
Frank Zappa