break, et cetera [long, but you can stop early]
Chris Torek
chris at umcp-cs.UUCP
Sun Nov 17 15:20:59 AEST 1985
In article <9500030 at iuvax.UUCP> cjl at iuvax.UUCP writes:
[example of a loop with pre- and post-conditions:]
> i = 0;
> /* Loop Invariant : (i <= HIGH+1) and X is not found in array[0..i-1] */
> while ( (i <= HIGH) && (array[i] <> X) {
> i++
> }
>
> if (i = HIGH+1) { /* X is not found in array[0..HIGH] */
> .... not found .....
> } else { /* (i < HIGH+1) and X is not found in [0..i-1] & (array[i]=X) */
> ... found .........
> }
>
> In contrast :
>
> for (i:=0; ++i; i>HIGH)
> if (array[i] = X) {
> break
> }
I am not sure how the `contrast' is supposed to read, but I can
guess what it would be as written in `real C' using break:
/*
* pre: for all k s.t. 0 <= k < HIGH, array[k] exists.
* inv: i < HIGH && for all k s.t. 0 <= k < i, array[k] != X.
* (Note that the invariant applies only in the conditional
* section of the for loop---not surprising, considering the
* `expanded' loop [a while statement, upon whose axiom we
* agree---I hope!].)
*/
for (i = 0; i != HIGH; i++)
if (array[i] == X)
break;
/*
* post: (i == HIGH && for all k s.t. 0 <= k < i, array[k] != X) ||
* (for all k s.t. 0 <= k < i, array[k] != X && array[i] == X).
* If you prefer: for all k s.t. 0 <= k < i, array[k] != X &&
* (i == HIGH || array[i] == X).
*/
This is, oddly enough, quite clear to me. Yet it would still be
so with the comparison to X inside the `for' condition.
I personally might even use a `Knuth-style goto', depending on
the situation:
for (i = 0; i < HIGH; i++)
if (array[i] == X)
goto found;
/* code to deal with `not found' */
return;
found:
/* code to deal with `found' */
return;
This has the benefit of separating the `or' part of the postcondition
without requiring an extra boolean. Plus if you act now---no, wait,
that was not what I meant---in addition, the goto-version sidesteps
the question of whether the `&&' and `||' in the postcondition are
short-circuiting. We would not want to accidently ask for array[HIGH],
would we? :-)
[Stop here if bored]
This discussion seems to be getting out of hand. I will close with
a copy of some particularly bad (but fast) code from one of my
production programs. I challenge someone to write a `more structured'
version that runs at least 95% as fast for a `typical' DVI file
when run on this Vax 785. (If you think you can improve this code
by expanding things in-line, think again: first, it makes changes
to the character-plotting code more difficult; but more importantly,
this routine just barely all fits in the cache, and that expansion
takes CPU time---about 15% more. This is why we have `unstructured'
constructs in `real' languages. Oh, and using an optimizing compiler
is not fair play! :-) )
[I hope you noticed that I changed the rules on you in that last
paragraph. If not, here is how: I said `at least 95% as fast'.
Speed is very often a consideration in `real programs', and at
least as often is not so when proving programs correct.]
/* This rather large routine reads the DVI file and calls on other routines
to do anything moderately difficult (except put characters: there is
a bunch of ugly code with `goto's which makes things much faster) */
ReadDVIFile () {
register int c,
p;
int advance;
ImFamily = -1; /* force imP_SetFamily command */
/* Only way out is via "return" statement */
for (;;) {
/* Get the DVI byte, and if it's a character, put it */
/* c = UnSign8 (getchar ()); */
c = getchar (); /* getchar() returns unsigned values */
if (DVI_IsChar (c)) { /* I know, ugly, but ... no function call
overhead this way */
register struct chinfo *ch;
register struct fontinfo *cf;
set:
advance = 1;
put:
cf = CurrentFont;
ch = &cf -> px -> px_info[c];
if (ch -> ch_width) {/* workaround for Imagen bug */
if (!cf -> cload[c])
DownLoadGlyph (c, ch, cf);
/* BEGIN INLINE EXPANSION OF ImSetPosition */
if (ImHH != hh) {
if (ImHH == hh - 1)
putchar (imP_Forw);
else if (ImHH == hh + 1)
putchar (imP_Backw);
else {
putchar (imP_SetHAbs);
putword (hh);
}
ImHH = hh;
}
if (ImVV != vv) {
putchar (imP_SetVAbs);
putword (vv);
ImVV = vv;
}
/* END INLINE EXPANSION OF ImSetPosition */
if (ImFamily != cf -> family) {
putchar (imP_SetFamily);
putchar (cf -> family);
ImFamily = cf -> family;
}
putchar (c);
ImHH += cf -> cwidth[c];
}
if (advance) {
hh += cf -> cwidth[c];
dvi_h += ch -> ch_TFMwidth;
p = SPtoDEV (dvi_h);
FIXDRIFT (hh, p);
}
continue;
}
/* Wasn't a character, maybe a font? */
if (DVI_IsFont (c)) {
SelectFont ((i32) (c - DVI_FNTNUM0));
continue;
}
/* Wasn't a font, see if it's a generic one */
if (p = DVI_OpLen (c)) {
/* It's generic, get its parameter */
switch (p) {
case 1:
p = Sign8 (getchar ());
break;
case 2:
fGetWord (stdin, p);
p = Sign16 (p);
break;
case 3:
fGet3Byte (stdin, p);
p = Sign24 (p);
break;
case 4:
fGetLong (stdin, p);
break;
case 5:
p = UnSign8 (getchar ());
break;
case 6:
fGetWord (stdin, p);
p = UnSign16 (p);
break;
case 7:
fGet3Byte (stdin, p);
p = UnSign24 (p);
break;
}
/* Now that we have the parameter, perform the command */
switch (DVI_DT (c)) {
case DT_SET:
c = p;
goto set;
case DT_PUT:
c = p;
advance = 0;
goto put;
case DT_RIGHT:
move_right:
dvi_h += p;
/* DVItype tells us that we must round motions in this way:
`When the horizontal motion is small, like a kern, hh
changes by rounding the kern; but when the motion is
large, hh changes by rounding the true position so that
accumulated rounding errors disappear.' */
if (p >= CurrentFont -> pspace ||
p <= CurrentFont -> nspace)
hh = SPtoDEV (dvi_h);
else {
hh += SPtoDEV (p);
p = SPtoDEV (dvi_h);
FIXDRIFT (hh, p);
}
break;
case DT_W:
dvi_w = p;
goto move_right;
case DT_X:
dvi_x = p;
goto move_right;
case DT_DOWN:
move_down:
dvi_v += p;
/* `Vertical motion is done similarly, but with the
threshold between ``small'' and ``large'' increased by a
factor of 5. The idea is to make fractions like $1\over2$
round consistently, but to absorb accumulated rounding
errors in the baseline-skip moves.' */
if (ABS (p) >= CurrentFont -> vspace)
vv = SPtoDEV (dvi_v);
else {
vv += SPtoDEV (p);
p = SPtoDEV (dvi_v);
FIXDRIFT (vv, p);
}
break;
case DT_Y:
dvi_y = p;
goto move_down;
case DT_Z:
dvi_z = p;
goto move_down;
case DT_FNT:
SelectFont ((i32) p);
break;
case DT_XXX:
DoSpecial (p);
break;
case DT_FNTDEF:
SkipFontDef (p);
break;
#ifdef PARANOID
default:
error (1, 0, "bad DVI_DT(%d): (%d)", c, DVI_DT (c));
#endif
}
continue;
}
/* Wasn't a char, wasn't a generic command, just pick it out from the
whole mess */
switch (c) {
case DVI_SETRULE:
SetRule (1);
break;
case DVI_PUTRULE:
SetRule (0);
break;
case DVI_NOP:
break;
case DVI_BOP:
BeginPage ();
break;
case DVI_EOP:
EndPage ();
if (!PFlag && PrevPagePointer == -1)/* was first page; done */
return;
break;
case DVI_PUSH:
dvi_stackp -> stack_hh = hh;
dvi_stackp -> stack_vv = vv;
dvi_stackp -> stack_dvi = dvi_current;
dvi_stackp++;
break;
case DVI_POP:
dvi_stackp--;
hh = dvi_stackp -> stack_hh;
vv = dvi_stackp -> stack_vv;
dvi_current = dvi_stackp -> stack_dvi;
break;
case DVI_W0:
p = dvi_w;
goto move_right;
case DVI_X0:
p = dvi_x;
goto move_right;
case DVI_Y0:
p = dvi_y;
goto move_down;
case DVI_Z0:
p = dvi_z;
goto move_down;
case DVI_PRE:
error (1, 0, "unexpected PRE");
case DVI_POST:
if (PFlag)
return;
error (1, 0, "unexpected POST");
case DVI_POSTPOST:
error (1, 0, "unexpected POSTPOST");
default:
error (1, 0, "undefined DVI opcode (%d)", c);
}
}
}
--
In-Real-Life: Chris Torek, Univ of MD Comp Sci Dept (+1 301 454 4251)
UUCP: seismo!umcp-cs!chris
CSNet: chris at umcp-cs ARPA: chris at mimsy.umd.edu
More information about the Comp.lang.c
mailing list