Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Posting-Version: version B 2.10.1 6/24/83; site umcp-cs.UUCP Path: utzoo!watmath!clyde!cbosgd!gatech!seismo!umcp-cs!chris From: chris@umcp-cs.UUCP (Chris Torek) Newsgroups: net.lang.c Subject: Re: break, et cetera [long, but you can stop early] Message-ID: <2246@umcp-cs.UUCP> Date: Sun, 17-Nov-85 00:20:59 EST Article-I.D.: umcp-cs.2246 Posted: Sun Nov 17 00:20:59 1985 Date-Received: Mon, 18-Nov-85 07:47:33 EST References: <771@whuxl.UUCP> <9500030@iuvax.UUCP> Organization: U of Maryland, Computer Science Dept., College Park, MD Lines: 312 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