Board index » delphi » Proving Program Correctness (was: Total: "for:" loop question...)

Proving Program Correctness (was: Total: "for:" loop question...)

Im Artikel <7f812v$207...@news.gate.net>, "Joe \"Nuke Me Xemu\" Foster"
<j...@bftsi0.UUCP> schreibt:

Quote
>I think the conflict here is over terminology.

Agreed.

Can you please define a 'correct program'?

I only found the definition "conforms to the specifications", and some related
keywords like Reliability, Integrity and Completeness.

Quote
>>Optimizing code is a different topic, isn't it?

>Hang on a sec, Martin's not talking about code optimization here.
>He's using US terminology having to do with verifying things that
>should remain true both before and after a computation. Loop
>invariants are properties that should remain true even during the
>computation.

A code optimizer can determine the structure of existing code, and create the
conditions from that code. Then it can e.g. find loop invariants, based on
these conditions, and rearrange the code for better performance. Since an
optimizer doesn't modify the overall behaviour of a program, I considered loop
invariants as a topic of optimization, not of correctness.

Quote
>> However, I do think

that some good has come out of the program-proofs crowd.<<

Agreed.

The intention of the early high level languages mainly was to ease the
translation of algorithms into executable code (Algol, Fortran...). The next
language generation added more tags and structures to the languages, like
'const', 'loop', data types, classes etc., that did not only simplify the
process of translating the algorithms into procedures, but also added more
abstract information and conditions to the code, so that the compiler could
detect more common mistakes. Where Basic or Fortran code contained lots of
GoTo's, the newer languages implemented structural statements, that allowed to
convert the former spaghetti code into structured code. (Though IMO a GoTo in
the right place sometimes can reduce the amount of code, even nowadays ;-)

The next generation of programming languages should include a further (more
abstract) description of the algorithms and conditions, that are to be
implemented in the code. Then the compiler itself could prove the correctness
of the code, far beyond what's possible with encapsulation in the currently
used OO languages.

Quote
>>it's been proven that there can be no

program that can determine whether every possible loop even stops<<

But in contrast to the halting problem, a program can at least verify that the
program *can* eventually stop, and that the according conditions *can* be met
somehow.

DoDi

 

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
> Can you please define a 'correct program'?

to me a correct program program is one that can be proven ( ;
no seriously, I think a good definition would be one that provides the appropriate
output for all possible instances of a given type(or a specific set of that type
if the input is limited as such).  This is the essence of a proof...you can't
possibly test for every integer because it is an infinite set(disregarding the
range of integers in a specific compiler implemementation of course), but you
*can* prove it...

The "appropriate output" depends on your program...it's pretty obvious I
think...if you don't know what the "appropriate output" is then you never should
have written the code in the first place...

Interrupts in DOS land and API calls and message handlers in Windows land
obviously don't apply

Quote
> (Though IMO a GoTo in
> the right place sometimes can reduce the amount of code, even nowadays ;-)

hmmm....give me a piece of code w/ a goto that can't be done with a while loop...
you can't...sorry

goto is an excuse for lazy/marginal programmers

watch:

while condition do
  begin
    {do some stuff}
    if badCondition then
     goto saveMeIAmAHack
    {do some more stuff}
  end;
label: saveMeIAmAHack {I'm not sure of the syntax here...I don't use goto}

I realize this is an oversimplified example...but all the examples of why goto is
necessary have been about this simple to solve...I'd love to see some code that
really "needed" a goto

ok, the {do some more stuff} code should be either nested in the if..then
statement or executed as a seperate procedure...
Actually, longer procedures tend to lead to more bugs in your code....a good
programmer tries to maintain a level of abstraction that prevents
bugs...optimizations are fine later...gotos are *never* fine, they breed bugs and
lead to spaghetti code(not to mention the implications when considering formal
proofs)

If any of you have worked with functional languages(like Haskell, ML, etc...) you
know what I'm talking about...

Quote
> >>it's been proven that there can be no
> program that can determine whether every possible loop even stops<<

hmmm...proven by whom?  please back this up, whoever wrote this

--
Statistics is the art of lying by means of figures.
- Dr. Wilhelm Stekhel

Experiments should be reproducible: they should all fail in the same way.
- Finagle's Rule

ka...@mindless.com ICQ 32283653

Re:Proving Program Correctness (was: Total: "for:" loop question...)


All you programming gurus really tickle me when you talk about GOT as being a
terrible sin in programming code.

The fastest language uses something quite similar to a goto...Yes, assembly
language has the JMP command ... now IMO when  you JMP somewhere in assembly
then in Essence you GOTO that place..right?

Re:Proving Program Correctness (was: Total: "for:" loop question...)


In article <371EBD02.EA3F3...@mindless.com>,
  Kathryn Taylor Jennings <ka...@mindless.com> wrote:
[...]

Quote
> > >>it's been proven that there can be no
> > program that can determine whether every possible loop even stops<<

> hmmm...proven by whom?  please back this up, whoever wrote this

   I'm not the person who wrote that (it _seems_ like VBDis is
quoting email - I can't find the person in the original thread.)
And I wouldn't put it quite this way. But my guess is that whoever
wrote it is referring to the unsolvability of the "halting problem".
Assuming we're talking about a Turing-complete language it's
impossible to write a routine

function Halts(SourceCode: string): Boolean;

that accepts arbitrary (syntactically valid) source code
as input and returns True if the program represented by
SourceCode terminates and False otherwise. I'd guess it
was proved by Turing - the proof is actually very simple.
Suppose you have a Halts function. You consider this routine:

procedure LiarParadox(SourceCode: string);
begin
  while Halts(SourceCode) do NOP;
end;

And now you run the LiarParadox routine, passing the
source code for LiarParadox as the SourceCode parameter.
What happens when you run LiarParadox(s), where s is
the source code for LiarParadox? If it halts then
the call to Halts must return True, because that's what
Halts does. But that means that the loop gets repeated,
and hence it doesn't halt. Otoh if it doesn't halt that
the reason must be that the loop gets executed infinitely
many times, in particular at least once. So Halts must be
returning True, which means it _does_ halt.

     So. LiarParadox(the code for LiarParadox) either halts
or it doesn't. If it does it doesn't, while if it doesn't
it does. That can't be right. So it must be that the
Halts function doesn't really exist. (So there's no perfect
de{*word*81}.)

-----------== Posted via Deja News, The Discussion Network ==----------
http://www.dejanews.com/       Search, Read, Discuss, or Start Your Own    

Re:Proving Program Correctness (was: Total: "for:" loop question...)


On Thu, 22 Apr 1999 01:09:09 -0500, Kathryn Taylor Jennings

Quote
<ka...@mindless.com> wrote:
>> (Though IMO a GoTo in
>> the right place sometimes can reduce the amount of code, even nowadays ;-)

>hmmm....give me a piece of code w/ a goto that can't be done with a while loop...
>you can't...sorry

>goto is an excuse for lazy/marginal programmers

>watch:

>while condition do
>  begin
>    {do some stuff}
>    if badCondition then
>     goto saveMeIAmAHack
>    {do some more stuff}
>  end;
>label: saveMeIAmAHack {I'm not sure of the syntax here...I don't use goto}

>I realize this is an oversimplified example...but all the examples of why goto is
>necessary have been about this simple to solve...I'd love to see some code that
>really "needed" a goto

You're not speaking to the point.  Sure, you can rewrite a piece of code
without goto's.  But you haven't demonstrated that it's important to do
so.  DoDi claims, and I claim, that a goto in the right place can
sometimes make a piece of code more efficient, or more readable.  The
fact that you can get rid of the goto isn't important; the question is
whether you can improve the code by doing so.

I've only used goto's twice in living memory.  Once, just recently, was
a random hack because I was too lazy to untangle a {*word*193} and relatively
unimportant function.  The other, though, was the result of days of
planning in which I decided--before writing a line of code--that heavy
use of goto's (51 of them in 720 lines of code) was the best way to
solve the problem.  You can rewrite that code without goto's, and I
don't care.  The code works, works right, and is readable.  I don't
think you'll improve it by rewriting it.

Quote
>> >>it's been proven that there can be no
>> program that can determine whether every possible loop even stops<<

>hmmm...proven by whom?  please back this up, whoever wrote this

Alan Turing.  Look up Halting Problem in one of your references.

--
"Oh, shootings.  Yes, but that doesn't mean Americans are more {*word*268}
than other people.  We're just better shots."

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
Kathryn Taylor Jennings wrote:
> hmmm....give me a piece of code w/ a goto that can't be done with a while loop...
> you can't...sorry

> goto is an excuse for lazy/marginal programmers

Sigh. Here we go again. Consider this:

label
  OutOfTheWholeLoop;
begin
  while SomeCondition do begin
    while SomeOtherCondition do begin
      while YetAnotherCondition do begin
        while HadEnoughLoops{?} do begin
          if SomeInnerCondition then goto OutOfTheWholeLoop;
        end;
      end;
    end;
  end;

  OutOfTheWholeLoop:
end;

If you'd like to remove the goto, be my guest:

var
  Flag: Boolean;
begin
  Flag := False;
  while SomeCondition do begin
    while SomeOtherCondition do begin
      while YetAnotherCondition do begin
        while HadEnoughLoops{?} do begin
          Flag := SomeInnerCondition;
          if Flag then Break;
        end;
        if Flag then Break;
      end;
      if Flag then Break;
    end;
    if Flag then Break;
  end;
end;

Which implementation do you choose? I choose (c) neither, because I like
it when languages have labeled break and continue blocks. (Java and Perl
have this, though I don't care for either of the languages themselves.)
In the event that we don't have labeled blocks, I choose the first.

Dave

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
Dave Shapiro wrote in message <371F93A0.9E492...@cfxc.com>...

>Kathryn Taylor Jennings wrote:
>> hmmm....give me a piece of code w/ a goto that can't be done with a
while loop...
>> you can't...sorry

>> goto is an excuse for lazy/marginal programmers

>Sigh. Here we go again. Consider this:

>label
>  OutOfTheWholeLoop;
>begin
>  while SomeCondition do begin
>    while SomeOtherCondition do begin
>      while YetAnotherCondition do begin
>        while HadEnoughLoops{?} do begin
>          if SomeInnerCondition then goto OutOfTheWholeLoop;
>        end;
>      end;
>    end;
>  end;

>  OutOfTheWholeLoop:
>end;

>If you'd like to remove the goto, be my guest:

>var
>  Flag: Boolean;
>begin
>  Flag := False;
>  while SomeCondition do begin
>    while SomeOtherCondition do begin
>      while YetAnotherCondition do begin
>        while HadEnoughLoops{?} do begin
>          Flag := SomeInnerCondition;
>          if Flag then Break;
>        end;
>        if Flag then Break;
>      end;
>      if Flag then Break;
>    end;
>    if Flag then Break;
>  end;
>end;

>Which implementation do you choose? I choose (c) neither, because I
like
>it when languages have labeled break and continue blocks. (Java and
Perl
>have this, though I don't care for either of the languages
themselves.)
>In the event that we don't have labeled blocks, I choose the first.

>Dave

I choose (c) also, but my (c) looks like this:

var
  Flag: Boolean;
begin
  Flag := False;
  while ((SomeCondition) and (not Flag)) do begin
    while ((SomeOtherCondition) and (not Flag))  do begin
      while ((YetAnotherCondition) and (not Flag))  do begin
        while ((HadEnoughLoops) and (not Flag)) do begin
          Flag := SomeInnerCondition;
        end;
      end;
    end;
  end;
end;

That's why it's called a pre-test loop, because you test the
conditions for execution before the loop begins. "Break" is a hack
too.

Scott

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote

>goto is an excuse for lazy/marginal programmers

Gotos are kind of like guns.  In the wrong hands they are dangerous.
Theoretically the world would be a better place without them. But, there are
conditions under which they are useful.  Even Wirth must have felt they were
necessary, otherwise why put them in the original Pascal definition?
Wirth/Jensen do say "The presence of a goto's in a Pascal program is often
an indication that the programmer has not yet learned "to think" in Pascal .
. .". The use of a goto does not, by itself, indicate "lazy/marginal"
programming.

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
David Rifkind wrote in message

<371f561c.2583...@netnews.worldnet.att.net>...

Quote
>On Thu, 22 Apr 1999 01:09:09 -0500, Kathryn Taylor Jennings
><ka...@mindless.com> wrote:
>>> (Though IMO a GoTo in
>>> the right place sometimes can reduce the amount of code, even
nowadays ;-)

>>hmmm....give me a piece of code w/ a goto that can't be done with a
while loop...
>>you can't...sorry

>>goto is an excuse for lazy/marginal programmers

>>watch:

>>while condition do
>>  begin
>>    {do some stuff}
>>    if badCondition then
>>     goto saveMeIAmAHack
>>    {do some more stuff}
>>  end;
>>label: saveMeIAmAHack {I'm not sure of the syntax here...I don't use
goto}

>>I realize this is an oversimplified example...but all the examples
of why goto is
>>necessary have been about this simple to solve...I'd love to see
some code that
>>really "needed" a goto

>You're not speaking to the point.  Sure, you can rewrite a piece of
code
>without goto's.  But you haven't demonstrated that it's important to
do
>so.

With all due respect, David, you haven't demonstrated that it's
important to write code _with_ goto's either. :-)

Quote
>  DoDi claims, and I claim, that a goto in the right place can
>sometimes make a piece of code more efficient, or more readable.  The
>fact that you can get rid of the goto isn't important; the question
is
>whether you can improve the code by doing so.

"Improving code" is a highly subjective and sometimes deeply religious
debate. It's unlikely that I'll change your mind, or that you'll
change mine. Not that either of us is particularly stubborn, it's just
too hard to prove one way or the other. It's mostly a matter of what
you consider "good" programming.

Quote
>I've only used goto's twice in living memory.  Once, just recently,
was
>a random hack because I was too lazy to untangle a {*word*193} and
relatively
>unimportant function.

So, here you say explicitly that it was a hack and you used it because
you were lazy. Hey, I'm not throwing stones, I'll wager that I'm
lazier that you are! :-)

Quote
>The other, though, was the result of days of
>planning in which I decided--before writing a line of code--that
heavy
>use of goto's (51 of them in 720 lines of code) was the best way to
>solve the problem.  You can rewrite that code without goto's, and I
>don't care.  The code works, works right, and is readable.  I don't
>think you'll improve it by rewriting it.

I'd like to have a look at it, if you don't mind. Email is fine so you
don't have to post the whole thing here (unless others are interested
also?).

Scott

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
Bruce Roberts wrote in message ...

>>goto is an excuse for lazy/marginal programmers

>Gotos are kind of like guns.  In the wrong hands they are dangerous.
>Theoretically the world would be a better place without them. But,
there are
>conditions under which they are useful.  Even Wirth must have felt
they were
>necessary, otherwise why put them in the original Pascal definition?

So that we could have these fun debates???

Quote
>Wirth/Jensen do say "The presence of a goto's in a Pascal program is
often
>an indication that the programmer has not yet learned "to think" in
Pascal .
>. .". The use of a goto does not, by itself, indicate "lazy/marginal"
>programming.

Agreed. I can be plenty "lazy/marginal" without using goto! :-)

Scott

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
Duncan Murdoch wrote:

> >Dave Shapiro wrote in message <371F93A0.9E492...@cfxc.com>...
> >>Sigh. Here we go again. Consider this:

> >>label
> >>  OutOfTheWholeLoop;
> >>begin
> >>  while SomeCondition do begin
>  ...
> >>          if SomeInnerCondition then goto OutOfTheWholeLoop;
>  ...
> >>  OutOfTheWholeLoop:
> >>end;

> On Thu, 22 Apr 1999 17:15:08 -0500, "Scott Roberts"
> <sgrob...@nospam-ionet.net> wrote:
> >I choose (c) also, but my (c) looks like this:

> >var
> >  Flag: Boolean;
> >begin
> >  Flag := False;
> >  while ((SomeCondition) and (not Flag)) do begin
>  ...
> >          Flag := SomeInnerCondition;
>  ...
> >end;

> I have to say I like Scott's solution better.  It's clearer.  In the

But it's not the same. A more elaborate version:

var
  Flag: Boolean;
begin
  Flag := False;
  while SomeCondition and not Flag do begin
    SomeCode;
    while AnotherCondition and not Flag do begin
      MoreCode;
      Flag := SomeInnerCondition;
      SomeCodeThatShouldntBeExecutedIfFlagIsTrue;
    end;
    EvenMoreCodeThatShouldntBeExecutedIfFlagIsTrue;
  end;
end;

As you can see, SomeCodeThatShouldnt... and EvenMoreCode... both get
executed because the test for breaking out of the loop is in the wrong
spot. You might be able to get around this with some judicious 'repeat's
or 'while True's or something, but at what point are you obfuscating
code just so you don't have to see the evil 'goto' in boldface, glaring
at you, mocking you, reminding you that you are an inferior coder? I'd
say it happened a ways back.

Dave

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
>Dave Shapiro wrote in message <371F93A0.9E492...@cfxc.com>...
>>Sigh. Here we go again. Consider this:
>>label
>>  OutOfTheWholeLoop;
>>begin
>>  while SomeCondition do begin
 ...
>>          if SomeInnerCondition then goto OutOfTheWholeLoop;
 ...
>>  OutOfTheWholeLoop:
>>end;

On Thu, 22 Apr 1999 17:15:08 -0500, "Scott Roberts"

Quote
<sgrob...@nospam-ionet.net> wrote:
>I choose (c) also, but my (c) looks like this:
>var
>  Flag: Boolean;
>begin
>  Flag := False;
>  while ((SomeCondition) and (not Flag)) do begin
 ...
>          Flag := SomeInnerCondition;
 ...
>end;

I have to say I like Scott's solution better.  It's clearer.  In the
first one, you say you're going to repeat those loops as long as some
conditions hold, and then you change your mind in the middle and jump
out.  You shouldn't lie like that!  If you're only planning to execute
the loop until something special happens, then that's what you should
write, and that's what Scott's code does write.

Duncan Murdoch

Re:Proving Program Correctness (was: Total: "for:" loop question...)


On Thu, 22 Apr 1999 17:25:36 -0500, "Scott Roberts"

Quote
<sgrob...@nospam-ionet.net> wrote:

>David Rifkind wrote in message
><371f561c.2583...@netnews.worldnet.att.net>...
[snip]
>>You're not speaking to the point.  Sure, you can rewrite a piece of
>code
>>without goto's.  But you haven't demonstrated that it's important to
>do
>>so.

>With all due respect, David, you haven't demonstrated that it's
>important to write code _with_ goto's either. :-)

I'm not sure how much respect you *should* have for someone who isn't
intelligent enough to stay out of a hopeless argument.  What I meant to
do was to point out that Ms. Jennings was not arguing to the point.  I
should have stopped there.

I had also intended to suggest that it's difficult to show a plausible
use of goto in a small example, except perhaps where efficiency is
critical; to argue for stylistic uses, you'll need to look at large,
complicated pieces of code.  But I neglected to make that point.

Quote
>>I've only used goto's twice in living memory.  Once, just recently,
>was
>>a random hack because I was too lazy to untangle a {*word*193} and
>relatively
>>unimportant function.

>So, here you say explicitly that it was a hack and you used it because
>you were lazy. Hey, I'm not throwing stones, I'll wager that I'm
>lazier that you are! :-)

I challenge you to a duel!  First one out of bed loses.

That sentence was written in the spirit of full disclosure.  I've
written plenty of indefensible code.  I've also written a small amount
of good code.  For some reason, it bothers me when people can't tell the
difference.

Quote
>>The other, though, was the result of days of
>>planning in which I decided--before writing a line of code--that
>heavy
>>use of goto's (51 of them in 720 lines of code) was the best way to
>>solve the problem.  You can rewrite that code without goto's, and I
>>don't care.  The code works, works right, and is readable.  I don't
>>think you'll improve it by rewriting it.

>I'd like to have a look at it, if you don't mind. Email is fine so you
>don't have to post the whole thing here (unless others are interested
>also?).

Translation: "Put your money where your mouth is."  Well, email me
(de-spam-proof my address) if you're really interested.

--
"Oh, shootings.  Yes, but that doesn't mean Americans are more {*word*268}
than other people.  We're just better shots."

Re:Proving Program Correctness (was: Total: "for:" loop question...)


Quote
NolenJ wrote:

> The fastest language uses something quite similar to a goto...Yes, assembly
> language has the JMP command ... now IMO when  you JMP somewhere in assembly
> then in Essence you GOTO that place..right?

Yes.... but compilers were invented fofr a reason ;-)

MH.

--
Martin Harvey.
http://www.harvey27.demon.co.uk/mch24/
Takeoff is optional.
Landing (sooner or later) is mandatory.

Go to page: [1] [2]

Other Threads