return in loop for ?

[yomgui]

hello,

is it legal to return inside a for loop
or am I obliged to break out of the loop before returning ?

thanks

yomgui

[Mike Meyer]

yomgui <no*@valid.org> writes:

is it legal to return inside a for loop
or am I obliged to break out of the loop before returning ?

Try it and see:

def f(): .... for i in range(20):
.... if i > 10: return i
.... print f() 11

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

[yomgui]

Mike Meyer wrote:

yomgui <no*@valid.org> writes:

is it legal to return inside a for loop
or am I obliged to break out of the loop before returning ?

Try it and see:

it is not because it does work on an implementation of python
that it will work on any other platform or in the futur.

yomgui

[Mike Meyer]

yomgui <no*@valid.org> writes:

Mike Meyer wrote:

yomgui <no*@valid.org> writes:

> is it legal to return inside a for loop
> or am I obliged to break out of the loop before returning ?

Try it and see:

it is not because it does work on an implementation of python
that it will work on any other platform or in the futur.

That's true no matter how you arrive at your answer.

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

[Steve Holden]

Mike Meyer wrote:

yomgui <no*@valid.org> writes:

Mike Meyer wrote:

yomgui <no*@valid.org> writes:

is it legal to return inside a for loop
or am I obliged to break out of the loop before returning ?

Try it and see:

it is not because it does work on an implementation of python
that it will work on any other platform or in the futur.

That's true no matter how you arrive at your answer.

But, to answer the specific question, there's nothing in the language
definition that suggests the programmer should refrain from using a
return inside a loop, so for any implementation to impose such a
restriction would be a violation of the language definition.

Yomgui: I am not a language lawyer, but I think you can feel safe
returning from inside a loop. Just as a matter of interest, how else
would you propose to implement the functionality Mike showed:

def f():

... for i in range(20):
... if i > 10: return i
...

Python is supposed to cleanly express the programmer's intent. I can;t
think of a cleaner way that Mike's - can you?

regards
Steve
--
Steve Holden [phone] [phone]
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[bonono]

Steve Holden wrote:

Yomgui: I am not a language lawyer, but I think you can feel safe
returning from inside a loop. Just as a matter of interest, how else
would you propose to implement the functionality Mike showed:

>>def f():

... for i in range(20):
... if i > 10: return i
...

Python is supposed to cleanly express the programmer's intent. I can;t
think of a cleaner way that Mike's - can you?

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

[Steve Holden]

bo****@gmail.com wrote:

Steve Holden wrote:

Yomgui: I am not a language lawyer, but I think you can feel safe
returning from inside a loop. Just as a matter of interest, how else
would you propose to implement the functionality Mike showed:

>>def f():

... for i in range(20):
... if i > 10: return i
...

Python is supposed to cleanly express the programmer's intent. I can;t
think of a cleaner way that Mike's - can you?

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

Well, I'm happy in this instance that practicality beats purity, since
the above is not only ugly in the extreme it's also far harder to read.

What are the claimed advantages for a single exit point? I'd have
thought it was pretty obvious the eight-line version you gave is far
more likely to contain errors than Mike's three-line version, wouldn't
you agree?

regards
Steve
--
Steve Holden [phone] [phone]
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[bonono]

Steve Holden wrote:

Well, I'm happy in this instance that practicality beats purity, since
the above is not only ugly in the extreme it's also far harder to read.

What are the claimed advantages for a single exit point? I'd have
thought it was pretty obvious the eight-line version you gave is far
more likely to contain errors than Mike's three-line version, wouldn't
you agree?

I thought it is about easier to spot error(that the return value is
done in single place) but didn't give too much attention as I don't buy
it. I call them "gotophobia"

[Duncan Booth]

Steve Holden wrote:

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

To bonono, not Steve:

So if a function should religiously have only one exit point why does the
example you give have two exit points? i.e. the 'return r', and the implied
'return None' if you execute the 'something' branch.
Well, I'm happy in this instance that practicality beats purity, since
the above is not only ugly in the extreme it's also far harder to read.

What are the claimed advantages for a single exit point? I'd have
thought it was pretty obvious the eight-line version you gave is far
more likely to contain errors than Mike's three-line version, wouldn't
you agree?

Arguments include: any cleanup code you need when returning from a function
is all in one place (mostly applicable to languages where you have to do
your own memory management---see the recent AST discussion on the python
dev list); or it stops you accidentally forgetting to return a value (as
demonstrated above :^) )

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.

[bonono]

Duncan Booth wrote:

To bonono, not Steve:

So if a function should religiously have only one exit point why does the
example you give have two exit points? i.e. the 'return r', and the implied
'return None' if you execute the 'something' branch. I may have remember it wrong, but don't ask me. I am not the one
advocate of it. Oh, you mean the something. It is that I forgot what it
was, the original one did have one return.
Arguments include: any cleanup code you need when returning from a function
is all in one place (mostly applicable to languages where you have to do
your own memory management---see the recent AST discussion on the python
dev list); or it stops you accidentally forgetting to return a value (as
demonstrated above :^) )

The faintly remember it was about the last reason, or why it has been
brought up.

[Neil Hodgson]

Steve Holden:

What are the claimed advantages for a single exit point? I'd have
thought it was pretty obvious the eight-line version you gave is far
more likely to contain errors than Mike's three-line version, wouldn't
you agree?

Single exit point is an ancient Dijkstraism. It was one of the
constraints that were thought to be useful in the early days of
structured programming. Having function flow always terminate at the end
of the function does make analysis simpler. It helps with, for example,
managing resource lifetimes: its easy to forget to release something
when you add a return statement.

Yes, the rule has obvious shortcomings, but OTOH if it had enabled
reasonable formal verification...

http://en.wikipedia.org/wiki/Structu...points_of_exit

Neil

[Fredrik Lundh]

Neil Hodgson wrote:

Yes, the rule has obvious shortcomings, but OTOH if it had enabled
reasonable formal verification...

I somehow find it hard to believe that you could write a multi-exit
function that cannot be trivially and automatically converted to a
single-exit function, for further analysis...

</F>

[Steve Holden]

Fredrik Lundh wrote:

Neil Hodgson wrote:

Yes, the rule has obvious shortcomings, but OTOH if it had enabled
reasonable formal verification...

I somehow find it hard to believe that you could write a multi-exit
function that cannot be trivially and automatically converted to a
single-exit function, for further analysis...

Besides which I'm somewhat sceptical about formal verification methods.

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; secondly the requirements sepcifications for
formal verification are way beyond what a normal user is capable of
specifying, making them an even worse tool for specification.

regards
Steve
--
Steve Holden [phone] [phone]
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Steven D'Aprano]

On Thu, 24 Nov 2005 11:06:58 +0000, Steve Holden wrote:

Besides which I'm somewhat sceptical about formal verification methods.

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;
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.

secondly the requirements sepcifications for
formal verification are way beyond what a normal user is capable of
specifying, making them an even worse tool for specification.

Can't argue with that observation :-)

--
Steven.

[Fredrik Lundh]

Steve Holden wrote:

sepcifications

did you mean: sceptifications ?

(otoh, with 11,100 google hits, "sepcifications" should probably be
considered as a fully acceptable alternate spelling ;-)

</F>

[Duncan Booth]

Steven D'Aprano wrote:

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;

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.)

[Peter Hansen]

Duncan Booth wrote:

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.

def funcWithGuaranteedOneExitPoint():
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]

Fredrik Lundh wrote:

Steve Holden wrote:

sepcifications

did you mean: sceptifications ?

(otoh, with 11,100 google hits, "sepcifications" should probably be
considered as a fully acceptable alternate spelling ;-)

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

[Scott David Daniels]

Fredrik Lundh wrote:

Steve Holden wrote:

sepcifications

did you mean: sceptifications ?

QOTW!

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

--Scott David Daniels
sc***********@acm.org

[Roy Smith]

"bo****@gmail.com" <bo****@gmail.com> wrote:

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

"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]

Duncan Booth <du**********@invalid.invalid> writes:

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.

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 <mw*@mired.org> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Mike Meyer]

Roy Smith <ro*@panix.com> writes:

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.

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 <mw*@mired.org> http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.

[Magnus Lycka]

Mike Meyer wrote:

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

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]

On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:

Steven D'Aprano wrote:

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;

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.)

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]

Steven D'Aprano wrote:

On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:

Steven D'Aprano wrote:

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;

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.)

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.

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 [phone] [phone]
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Steve Holden]

Steven D'Aprano wrote:

On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:

Steven D'Aprano wrote:

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;

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.)

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.

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 [phone] [phone]
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Steven D'Aprano]

On Fri, 25 Nov 2005 08:36:48 +0000, Steve Holden wrote:

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.)

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.

There seems to have been some misattribution in recent messages, since I
believe it was *me* who raised doubts about a program verifying itself.

Fair enough.
This has nothing to do with the Halting Problem at all.
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.

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.
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.

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

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]

Steven D'Aprano wrote:

On Fri, 25 Nov 2005 08:36:48 +0000, Steve Holden wrote: [...]

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

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.

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.
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.
Well naturally I can't stop you thinking that, so I won't try.
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.

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 characterisation of the state of the art.

regards
Steve
--
Steve Holden [phone] [phone]
Holden Web LLC www.holdenweb.com
PyCon TX 2006 www.python.org/pycon/

[Duncan Booth]

Steven D'Aprano wrote:

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.

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]

Duncan Booth enlightened us with:

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.

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

[Steven D'Aprano]

On Mon, 28 Nov 2005 08:44:04 +0000, Duncan Booth wrote:

Steven D'Aprano wrote:

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.

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.

Yes, of course. By saying "no guarantee" I was guilty of understatement:
at the very least, we can guarantee that the verifier will *not* correctly
verify every possible program. (Which of course is no different from human
programmers.)

--
Steven.

[Steven D'Aprano]

On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote:

Duncan Booth enlightened us with:

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.

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.

No, that is not right -- it is easy to create a program to determine
whether *some* programs will terminate, but it is impossible to create a
program which will determine whether *all* programs will terminate.
--
Steven.

[Mike Meyer]

Steven D'Aprano <st***@REMOVETHIScyber.com.au> writes:

On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote:

Duncan Booth enlightened us with:

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.

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.

No, that is not right -- it is easy to create a program to determine
whether *some* programs will terminate, but it is impossible to create a
program which will determine whether *all* programs will terminate.

Which means you can't create a verifier which will verify all
programs. Is there a reason to believe that you can't have a verifier
with three possible outcomes: Correct, Incorrect, and I don't know,
and it is always correct in doing so? Note that "I don't know" could
be "I ran longer than I think is reasonable and gave up trying."

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

[Mike Meyer]

Paul Rubin <http://ph****@NOSPAM.invalid> writes:

Mike Meyer <mw*@mired.org> writes:

Which means you can't create a verifier which will verify all
programs. Is there a reason to believe that you can't have a verifier
with three possible outcomes: Correct, Incorrect, and I don't know,
and it is always correct in doing so? Note that "I don't know" could
be "I ran longer than I think is reasonable and gave up trying."

It's trivial to write such a verifier, if you get my drift.

Almost as cute as the simplest self-replicating shell script.

Ok, so it's possible. Are there any useful examples? Does the BCPL
type verifier count?

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

[Steven D'Aprano]

On Mon, 28 Nov 2005 12:05:03 -0500, Mike Meyer wrote:

Steven D'Aprano <st***@REMOVETHIScyber.com.au> writes:

On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote:

Duncan Booth enlightened us with:
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.
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. No, that is not right -- it is easy to create a program to determine
whether *some* programs will terminate, but it is impossible to create a
program which will determine whether *all* programs will terminate.

Which means you can't create a verifier which will verify all
programs.

I thought that's what I said originally *wink*
Is there a reason to believe that you can't have a verifier
with three possible outcomes: Correct, Incorrect, and I don't know,
and it is always correct in doing so? Note that "I don't know" could
be "I ran longer than I think is reasonable and gave up trying."

That seems perfectly reasonable to me.

I don't know about anyone else in this discussion, but I'm talking about
*theoretical* source code verification of formal correctness. In
*practice*, I don't know what the state of the art is, but I suspect it
will be a long, long time before it is as easy as running "import
mymodule; verify(mymodule)".
--
Steven.

[Paul Rubin]

Mike Meyer <mw*@mired.org> writes:

Which means you can't create a verifier which will verify all
programs. Is there a reason to believe that you can't have a verifier
with three possible outcomes: Correct, Incorrect, and I don't know,
and it is always correct in doing so? Note that "I don't know" could
be "I ran longer than I think is reasonable and gave up trying."

It's trivial to write such a verifier, if you get my drift.

Almost as cute as the simplest self-replicating shell script.

Ok, so it's possible. Are there any useful examples? Does the BCPL
type verifier count?

The trivial verifier simply prints "I don't know" for EVERY program
you input. It is never wrong.

I don't know about the BCPL type verifier but every statically typed
language verifies certain assertions about the types of expressions
and this is useful. I think I heard that the Hindley-Milner algorithm
always succeeds (not sure what the conditions are for that) but that
it can take exponential time for some pathological cases. The
incompleteness theorem says there are undecidable problems in any
system complex enough to include Peano arithmetic. So if the
Hindley-Milner algorithm always succeeds, it just means that type
systems aren't complex enough to express arithmetic in.

I don't really know enough about this type stuff to discuss it
sensibly at the moment. There's a book I want to read, "Types and
Programming Languages" by Benjamin Pierce, which is supposed to
explain it pretty well. It's supposed to be excellent. But I haven't
had a chance to sit down with a copy yet.

http://www.cis.upenn.edu/~bcpierce/tapl/

[Paul Rubin]

Steven D'Aprano <st***@REMOVETHIScyber.com.au> writes:

I don't know what the state of the art is, but I suspect it
will be a long, long time before it is as easy as running "import
mymodule; verify(mymodule)".

Some pretty significant pieces of software have been formally verified
to meet their formal specifications. The trouble with
"verify(mymodule)" is that usually means something closer to "verify
that mymodule does what I hope it does". The computer does not yet
have a telepathy peripheral that can read your mind and figure out
what you are hoping, and people's attempts to express formally what
they are hoping are easily wrong just like programs are often wrong.

[Mike Meyer]

Paul Rubin <http://ph****@NOSPAM.invalid> writes:

I don't know about the BCPL type verifier but every statically typed
language verifies certain assertions about the types of expressions
and this is useful.
BCPL is untyped. You can perform any operation on any variable. You
can use the floating point add op on a pair of ints, or a pair of
function pointers. It doesn't care - it doesn't know what types the
variables are.

The type verifier extracted type information from context, and
propogated that through the system to look for places where the
programmer applied an operation to a type for which it was
inappropriate. It found bugs in itself.
I don't really know enough about this type stuff to discuss it
sensibly at the moment. There's a book I want to read, "Types and
Programming Languages" by Benjamin Pierce, which is supposed to
explain it pretty well. It's supposed to be excellent. But I haven't
had a chance to sit down with a copy yet.

I've been looking through it. It deals with type correctness, and by
association, evalulation completion. There are some fairly complex
systems in it. He does promise to reveal the features of programming
languages that cause the programs (or their type validation) to fail
to terminate.

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

[Alex Martelli]

Paul Rubin <http://ph****@NOSPAM.invalid> wrote:

Steven D'Aprano <st***@REMOVETHIScyber.com.au> writes:

I don't know what the state of the art is, but I suspect it
will be a long, long time before it is as easy as running "import
mymodule; verify(mymodule)".

Some pretty significant pieces of software have been formally verified
to meet their formal specifications. The trouble with
"verify(mymodule)" is that usually means something closer to "verify
that mymodule does what I hope it does". The computer does not yet
have a telepathy peripheral that can read your mind and figure out
what you are hoping, and people's attempts to express formally what
they are hoping are easily wrong just like programs are often wrong.

Yep. I'm reminded of an ambulance dispatch system (read about it a long
time ago on the Risks mailing list, so I might be off on the detail, but
the gist should be correct) which was formally proven to obey a long
list of rules, one of which was "for this kind of emergency, an
ambulance must arrive within 10 minutes" (or the like).

Problem, of course, being that in formal logic this implies "if this
kind of emergency exists and no ambulance has arrived within 10 minutes,
you have an impossibility and from an impossibility ANY theorem can be
proven". So, if real-world road conditions meant the ambulance was
about to arrive in 10 minutes and 5 seconds, it might instead be
rerouted elsewhere... not having arrived in 10 minutes, a contradiction
was in the system and it could prove anything (I think that's know as
the theorem of Pseudo-Scotus). It's hard in (classic) logic to express
"this MUST be true; if it's false, ..." -- to human beings the first
"MUST" can be interpreted as "99.9% probability" or the like, so the "if
it's false" clause is meaningful ("in the extremely unlikely, but not
impossible since nothing's truly impossible in the real world, situation
that it's false, ..."), but to Aristotle's logic, if something MUST be
true, it's obviously irrelevant whatever might follow if that something
were instead to be false.
Alex