chris@umcp-cs.UUCP (Chris Torek) (11/17/85)
In article <9500030@iuvax.UUCP> cjl@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@umcp-cs ARPA: chris@mimsy.umd.edu
mikes@3comvax.UUCP (Mike Shannon) (11/20/85)
Chris Torek in the cited article: > 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; --- How about some background on 'Knuth-stype goto's? I've run across this style before, where there is some sort of descriptive label every 5 or 6 lines. And lots of goto's. Does Knuth like these? Do you like these? What could recommend this style to anyone? I can't say I like it very much. -- Michael Shannon {ihnp4,hplabs}!oliveb!3comvax!mikes
zben@umd5.UUCP (11/22/85)
In article <285@3comvax.UUCP> mikes@3comvax.UUCP (Mike Shannon) writes: >Chris Torek in the cited article: >> 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; > How about some background on 'Knuth-stype goto's? I've run across >this style before, where there is some sort of descriptive label every >5 or 6 lines. And lots of goto's. > Does Knuth like these? Do you like these? What could recommend >this style to anyone? I can't say I like it very much. > Michael Shannon {ihnp4,hplabs}!oliveb!3comvax!mikes No, no, stop! DON'T tell them about GOTOs until they have demonstrated that they have decisively broken the "more is better" syndrome! Or else it's going to be spaghetti time again. Ya know, I think I read a science fiction story once with this same plot. Or was it calculators? ... :-) -- Ben Cranston ...{seismo!umcp-cs,ihnp4!rlgvax}!cvl!umd5!zben zben@umd2.ARPA