address of a statement in C

[dandelion]

You haven't. You may think so, you may even have paid no attention
to them, but they are there. Without [invariants], programming is
impossible, after all.

I think you really need to take a leaf from Knuth here:

"Beware of bugs in the above code; I have only proved it
correct, not tried it."

Yes. I know that one (Thanks to /usr/bin/games/fortune).

As I believe David Parnas has noted as well, program proofs usually
embed deliberate simplifications, lest the proof be as complex as
(or more complex than) the program itself.

I surmise it's usually the latter. However, I wasn't talking of proving
correctness

That depends -- on what is on line 14, among other things. Even
if line 14 is something like:

p = &zog;

Ok. But then again, that is not what I meant. Sorry for my sloppy wording,
sometimes.

That should (of course) have read "at the end of the loop. That is, prior to
the execution of the code on line 14.

the value that one "sees" in i might change.

if &i == p. Correct. But outside the scope of the example.

In a debugger, for
instance, I might well find that i suddenly becomes 0xa0c9e7d4,
because it shares a register with variable "p" in the underlying
(optimized) machine code.

Also correct. But with the remark that using an debugger on optimized code
isn't the way to see what's happening to individual variables. For the
reason you specify.

On the other hand, if line 14 is:

printf("i is now %d\n", i);

I *would* expect to see "i is now 10" in the output, and if I did
not, I could use whatever additional information I had about the
system to try to find out why not.

That would be either a compiler bug and/or a hardware bug. I cannot really
imagine a well functioning system (hw&os&compiler) screwing up so basic a
loop. Unless (of course) it's a multithreaded program and 'i' is global, or
an IRQ screwed up, or (i've allredy read all your post) Alpha
particles/cosmic radiation or an insect crawling around in your system
(Eniac).

These *are* good things -- but remember:
Sometimes designs fail.

As Bradley Sherman asked:

Can you prove that electromigration will not cause a fault in
the processor or gamma radiation will not alter a bit [...]?

You can't. After all physics is physics is nasty...

(We used to have memory chips with alpha-particle problems. Bits
stored in memory would change. Tim May is fond of telling the
story of how he figured this out. "Hot electron migration" remains
a problem in semiconductor design, too. I have stories about timing
problems in various CPUs, such as the carry-chain propagation bug
in the VAX, or the bug in the Ultrasparc CPU where the forwarding
logic would sometimes write an ALU computation into the wrong
register.)

Right you are. Thanks for the interesting story. I though my
"ghost-characters" coming in over an RS485 line were wild... It turned out
there ws this *huge* fridge right next to it.

However, the response was to someone who claimed to have written software
*without* invariants and my response was intended merely to show this is not
possible.

 

[dandelion]

It's tautological, as I and others have noted. As such it has no
meaningful consequence.


Ah, the "semantics" defense, typically the final resort of those who
cannot formulate a coherent argument in support of their position.

Ok. I'll rephrase more clearly..

A goto for wich an alternative exists withing the requirements of the code,
indicates bad code.

That better?

 

[Tim Rentsch]

Oh. Does this mean you believe that using 'goto' *is* substantially
different from using 'break' and 'return', and try to avoid using
'goto' when possible?

I'd avoid the term "substantially different",

[... explanatory comments snipped ...]

I adopt no mottoes about "trying to avoid".

Yes, that's what I thought. Hence my original statement.

 

[Thomas Stegen]

and if you wrote

9 i=0;
10 while(i<10)
11 {
12 i++;
13 }

You would expect i to be 10 on line 14, would you not?

Welcome to the loop-invariant.

That is not what a loop invariant is. Though you can conclude that
from the loop invariants in this case.

The loop invariant is that i <= 10. Other invariants are that i < 100
for example, but that is irrelevant since i <= 10 is stricter.

As an aside, note that loop invariants does not need to be true during
the execution of the loop, only during the test.

 

[Arthur J. O'Dwyer]

static char buffer[1000];
char *p, *pstart;
while (fgets(buffer, sizeof buffer, in) != NULL) {
for (p=buffer; isspace(*p); ++p) continue;
if (!strncmp(p, "%%MERR", 6)) goto all_done;

[...]
Just offhand, how about refactoring this way:

while( (p = next_input_nonblank( buffer, sizeof buffer, in ))
&& strncmp( p, "%%MERR", 6 ) != 0
){
...
}

where 'next_input_nonblank()' is a small function that does both the
'fgets()' and the loop skipping blanks (assuming there is input to
process). That gets rid of the need to have any intermediate loop
exit. If the variable 'p' isn't used after the loop exits, then

while( p = next_valid_input( buffer, sizeof buffer, in ) ){
...
}

is another possible refactoring.

Both are decent and equivalent refactorings. But I feel about functions
the way you do about 'goto': I can tell at a glance what 'fgets...
while(isspace(...)) continue;' is doing, but with either of your
refactorings I'd have to go find out what 'next_valid_input' was doing
to my input stream before I'd be comfortable continuing.

Either

while( fgets( buf, sizeof buf, fp ) != NULL ){
do {
process( buf );
} while( have_buffered_input( buf ) );
}

I don't think that works with the less drastically simplified original
version, though. The original (still simplified, but less so) is more
like

while (fgets(buf, sizeof buf, fp) != NULL) {
top_of_loop:
for (p=buffer; isspace(*p); ++p) ;
if (!strncmp(p, "%%MERR", 6)) goto all_done;
for (p += 6; isspace(*p); ++p) ;

if (stprefix(buf, "%classdef")) {
retrieve_class_name();
strcpy(buf, retrieve_class_members_and_\
return_following_line(fp, &local_struct));
goto top_of_loop;
}
else if (stprefix(buf, "%token")) {
[...]
}
[...]
}

Your refactoring may still be applicable, but IMVHO it would end up
separating some parts of the program that ought to be together, or vice
versa.

(The whole program is at
http://www.contrib.andrew.cmu.edu/~ajo/free-software/ocamlmerr/ocamlmerr.c
if you want to look at the absolutely unsimplified version. I agree
it's very messy, I just like my solutions better than yours so far.
Maybe my position would be that your solutions make an intrinsically
unstructured passage /look/ structured (by clever use of &&, break,
do-while, etc.), which would end up confusing me more than if it was just
left looking hairy! At least then the reader knows to be careful!

-Arthur

 

[Arthur J. O'Dwyer]

You haven't. You may think so, you may even have paid no attention to them,
but they are there. Without them, programming is impossible, after all.

Yes, and writing a term paper in American history is impossible without
quantum mechanics. Without quantum mechanics, your pencil would fall
apart, after all! But that doesn't mean a history student needs to pay
any attention to QM in order to write a perfectly fine term paper;
likewise, it's possible to write a perfectly fine computer program without
paying any attention to invariants or type theory or any of the often-
bizarre theories computer scientists have invented.

For instance if on one fine line of code you write
10 a=10;
you would expect A to be 10 in the code on line 11, no?

Depends on the language, of course.

Well... That's the assignment invariant.

A programmer would probably call that the "common sense." You
see?

Have a nice snigger while you remember that both your CPU and your
compiler have been carefully designed to honour invariants.

...Unless you run MSVC on an Intel. ;-)

-Arthur

 

[dandelion]

Yes, and writing a term paper in American history is impossible without
quantum mechanics.

Not true. Writing a history paper was possible long before QM was invented.
After
all Tacitus write the Historiae and Annales well before that.

Without quantum mechanics, your pencil would fall
apart, after all!

Ah yes... And apples did not fall until Newton wrote the Principia.

But that doesn't mean a history student needs to pay
any attention to QM in order to write a perfectly fine term paper;

Now, the person in question is not a history student confronted with
Schroedinger,
Heissenberg, Planck et al. but someone pretend^H^H^H^H^H^Hclaiming to be a
"professional", speaking in a forum dedicated to the subject. That's quite a
different
situation, isn't it?

So if aa history student claims (s)he wrote a thesis without any QM
involved, i tend
not to be surprized. If however a physics student, during a discusion about
QM makes
the same claim, (s)he deserves to be corrected.

likewise, it's possible to write a perfectly fine computer program without
paying any attention to invariants or type theory or any of the often-
bizarre theories computer scientists have invented.

Without paying attention... All too true. I've seen many examples. But that
was not
the claim Mr Bos made. After all he wrote software *without* invariants.

Depends on the language, of course.

And which language do you have in mind? Tell me and i'll
rework the example to match (provided i know the language, of course).
Even PostScript has it's invariants.

A programmer would probably call that the "common sense." You
see?

I see. I call it common sense, too. But i did not want to make it *that*
hard
for Mr. Bos, who did not study at the RUG, after all.

Thanks to all the guys who worried about invariants too much. That's why I
like to point out you cannot write programs without invariants as Mr Bos
claimed
to have done.

Now if people call a penis a dick, does that mean penises don't exist? I
would
even go as far as to call some people acorns eventhough they don't hang on
trees
and are known in biology as Homo Sapiens.

By the way... It is considered impolite (if not dishonest) to snip without
marking in
some places. It also occurs to me that you *snipped* the not-so-common-sense
example.

...Unless you run MSVC on an Intel. ;-)

As has been pointed out by another poster: design can fail. There are
preciously
few processors or compiler totally bug-free.

dandelion.

 

[Richard Bos]

I don't think that works with the less drastically simplified original
version, though. The original (still simplified, but less so) is more
like

while (fgets(buf, sizeof buf, fp) != NULL) {
top_of_loop:
for (p=buffer; isspace(*p); ++p) ;
if (!strncmp(p, "%%MERR", 6)) goto all_done;
for (p += 6; isspace(*p); ++p) ;

if (stprefix(buf, "%classdef")) {
retrieve_class_name();
strcpy(buf, retrieve_class_members_and_\
return_following_line(fp, &local_struct));
goto top_of_loop;

That's hardly an argument for goto, though; wouldn't continue work just
as well? If there'd been another nested loop in between, it would've
been a better example.

Richard

 

[dandelion]

That is not what a loop invariant is. Though you can conclude that
from the loop invariants in this case.

Correct. It's the post-condition for the loop. I should have said "You would
expect 0 <= i < 10 inside the loop. But hey...

I was busy *and* tired.

The loop invariant is that i <= 10.

Incomplete. See above.

Other invariants are that i < 100
for example, but that is irrelevant since i <= 10 is stricter.

The latter implies the former and makes little sense.

As an aside, note that loop invariants does not need to be true during
the execution of the loop, only during the test.

You can screw the loop invariant easily by adding i++ somewhere in the loop,
but that's something i'd consider (ipso facto) bad coding practice,
allthough it's sadly far from uncommon.

 

[dandelion]

Ah, so you are indeed urging us to eschew break (except in switch
cases) and return (except at the end of a function), which is
essentially what I claimed in my original response.

I'm not urging you to do anything. It's a free world. If you ask for my
opinion you'll get it, wether you are happy with it or not.

Note that you claimed goto's effect on invariants is "inherent".

Almost. It is (theoretically) possible to employ goto's without braking any
invariants, but I hardly see the point in doing so.

Of course this is only true if a goto occurs in the scope of some
invariant.

Ummm... When programming you are *always* in the scope of some invariant or
other. Even if it's the very basic process invariant (if the code gets
executed, you process/thread/fibre is running).

Which (of course) is perfectly common sense until you write your own
multi-threading library.

It is equally true if a (non-switch) break or return
occurs in such scope. Thus my claim that your claim is just as
true of the latter two as it is of goto stands.

Whatever. Either return and break (non-switch) have well difined effects on
the invariant: the former just chucks it out of the window (Invariant? What
invariant?), the latter only modifies the post-condition of a loop and
terminates early so the rest of the loop does not suffer. A goto statement,
in contrast, has no such defined effects, you can just jump anywhere with
unspecified, nay, undefined effects on any invariant.

Hence there is a (rather big) difference.

For the record, I too prefer to avoid using break to escape from
loops with non-trivial conditions or bodies (that is, in any case
where the "hidden invariant" created by break isn't readily apparent
to the reader), and I prefer a single point of return from non-
trivial functions.

Then we agree on that. I just solved a little puzzle where an early return
was used and therefore he interrupt-enable wasn't set as it should have
been. Since it played inside an ISR and the effects weren't immediate (the
next interrupts just don't arrive) the goings-on were *very* vague.

However, I do not use those preferences to
justify sweeping generalizations about what control structures are or
are not problematic, and in particular I do not discriminate against
one such control structure when it has the same consequences as the
others.

Well.. As I pointed out above, goto is a lot worse than break or return,
since
*no* rules apply and there is *no* defined consequence for your invariants.

Hence your claim about my claim falls.

Thank you.

 

[dandelion]

Incomplete. See above.

Sorry... Incorrect! It's i<10.

And 0<=i<10 includes the assignment invariant for "i=0", which (technically)
is not corret either.

 

[Thomas Stegen]

You can screw the loop invariant easily by adding i++ somewhere in the loop,
but that's something i'd consider (ipso facto) bad coding practice,
allthough it's sadly far from uncommon.

It's not bad coding practice at all. Loop invariants are not meant to
be true at all times in a loop. A loop invariant is defined as something
that is true during every test of the loop condition.

I have seen no one except you call this bad coding practice, do you have
any references please.

 

[Thomas Stegen]

Sorry... Incorrect! It's i<10.

No, that is false on one of the looop condition tests, thereby excluding
it from being a loop invariant. It is not complete though. I should have
said _a_ loop invariant is ... since a loop can have many invariants.

 

[Thomas Stegen]

That's hardly an argument for goto, though; wouldn't continue work just
as well? If there'd been another nested loop in between, it would've
been a better example.

Well the test condition won't be executed using the goto, whereas
continue would cause the condition to be tested. And since fgets
has side effects it matters in this case.

 

[dandelion]

It's not bad coding practice at all.

Where I work it is.

Loop invariants are not meant to be true at all times in a loop.

Hmmm... There seems to be a slight difference of definitions here...

A loop invariant is defined as something
that is true during every test of the loop condition.

Ummm... No. See (for instance)

http://courses.cs.vt.edu/~cs3304/Spring00/notes/Chapter-3b/tsld015.htm

<quote>
I must meet the following conditions:

1. P => I (the loop invariant must be true initially)
2. {I} B {I} (evaluation of the Boolean must not change the validity of I)
3. {I and B} S {I} (I is not changed by executing the body of the loop)
4. (I and (not B)) => Q (if I is true and B is false, Q is implied)
5. The loop terminates (can be difficult to prove)
</quote>

The invariant is called I, P is the precondition, Q is the postcondition.
Mind [3].

As to the "bad coding practice" I gave a bad example. So that statement is
hereby retracted. Adding i++ in the loop isn't bad coding perse (it may be
part of the invariant). Modifying the loop-invariant in the loop is.

 

[dandelion]

No, that is false on one of the looop condition tests, thereby excluding
it from being a loop invariant.

Nope. See my other post and (more specifically) there reference contained
therein. The invariant *must* be true in the *body* of the loop, i<10
satisfies that, i<=10 does not, since within the body of the loop i never
reaches the value of 10.

It is not complete though. I should have
said _a_ loop invariant is ... since a loop can have many invariants.

In a loop more than one invariant can be valid, as usually is the case (but
not always). However, *the* loop-invariant is no more than i<10 in this
case. Preconditions and postconditions can be less restrictive, though.

 

[dandelion]

No, that is false on one of the looop condition tests, thereby excluding
it from being a loop invariant.

Correct. I hope you do not respond to one of the posts I just cancelled. If
you do, apologies.

 

[pete]

Hmmm... There seems to be a slight difference of definitions here...


Ummm... No. See (for instance)

Do you suppose that loop invariants
might be on topic in comp.programming?

 

[Thad Smith]

Do you suppose that loop invariants
might be on topic in comp.programming?

Yes, an invariant is true where postulated, which is at discrete
points. In general, there are multiple variables involved in the
invariant, which can be changed at different times in the loop body.
Between starting and finishing the transition of one state to another,
the invariant at the beginning of the transition no longer holds.

It would be possible to specify other invariant conditions between the
steps of the loop body. This is useful for complex transformations.
These intermediate invariant conditions would not, in general, be the
same as the loop invariant.

Thad

 

[blmblm]

"True during every test of the loop condition" is not the same as
"true at all times in a loop", right?

I hadn't thought of the "true during every test ...." definition,
but it does seem to be consistent with the usual definition (something
that, if true before execution of the loop body, is true still/again
after execution of the loop body).

Yes, an invariant is true where postulated, which is at discrete
points. In general, there are multiple variables involved in the
invariant, which can be changed at different times in the loop body.
Between starting and finishing the transition of one state to another,
the invariant at the beginning of the transition no longer holds.

It would be possible to specify other invariant conditions between the
steps of the loop body. This is useful for complex transformations.
These intermediate invariant conditions would not, in general, be the
same as the loop invariant.

Seconded, or something.