* Re: Should internet support software be written in Ada?
@ 1995-03-17 0:24 Bill Brooks
1995-03-17 8:47 ` Anthony Shipman
` (7 more replies)
0 siblings, 8 replies; 76+ messages in thread
From: Bill Brooks @ 1995-03-17 0:24 UTC (permalink / raw)
In article <2F5B780E@SMTPGATE2.STRATCOM.AF.MIL>,
Bennett, Chip (KTR) ~U <BennettC@J64.STRATCOM.AF.MIL> wrote:
> [...stuff deleted..]
>
>Point 2: I going to make a huge leap here and assume that httpd is written
>in C. [...stuff deleted..]
> Comments?
>
>Chip Bennett
Yep. Here's a representative sample of the code that comes with NCSA's
httpd (everything including the formatting is from the original):
----------------------- start paste --------------------------
*/
if (strchr(mapname,'/')) {
strcpy(conf,getenv("PATH_TRANSLATED"));
goto openconf;
}
if ((fp = fopen(CONF_FILE, "r")) == NULL)
servererr(strcat("Couldn't open configuration file:", CONF_FILE));
while(!(getline(input,MAXLINE,fp))) {
char confname[MAXLINE];
if((input[0] == '#') || (!input[0]))
continue;
for(i=0;isname(input[i]) && (input[i] != ':');i++)
confname[i] = input[i];
confname[i] = '\0';
if(!strcmp(confname,mapname))
goto found;
}
----------------------- end paste ---------------------------
In the rich tradition of discussing good software engineering practices in
c.l.a(regardless of language) I'll ask: is this good coding style?
Keep in mind that this code was written under the auspices of one of
the top 5 schools in CS in the United States.
--
"Bright young men of disheveled appearance, often with sunken glowing
eyes...their fingers, already poised to strike, at the buttons and
keys on which their attention seems to be riveted as a gambler's on
the rolling dice." -Joseph Weizenbaum on "compulsive programmers"
^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-17 0:24 Should internet support software be written in Ada? Bill Brooks @ 1995-03-17 8:47 ` Anthony Shipman 1995-03-19 22:06 ` David Weller ` (6 subsequent siblings) 7 siblings, 0 replies; 76+ messages in thread From: Anthony Shipman @ 1995-03-17 8:47 UTC (permalink / raw) In <3kaksj$iur@isnews.calpoly.edu> wbrooks@hertz.elee.calpoly.edu (Bill Brooks) writes: >In the rich tradition of discussing good software engineering practices in >c.l.a(regardless of language) I'll ask: is this good coding style? >Keep in mind that this code was written under the auspices of one of >the top 5 schools in CS in the United States. I've noticed that academics seem to write terrible code (from a software engineering point of view), compared with professionals who do it for a living. -- Anthony Shipman "You've got to be taught before it's too late, TUSC Computer Systems Pty Ltd Before you are six or seven or eight, To hate all the people your relatives hate, E-mail: als@tusc.com.au You've got to be carefully taught." R&H ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-17 0:24 Should internet support software be written in Ada? Bill Brooks 1995-03-17 8:47 ` Anthony Shipman @ 1995-03-19 22:06 ` David Weller 1995-03-23 15:05 ` Theodore Dennison ` (3 more replies) 1995-03-22 23:08 ` Should internet support software be written in Ada? Keith Thompson ` (5 subsequent siblings) 7 siblings, 4 replies; 76+ messages in thread From: David Weller @ 1995-03-19 22:06 UTC (permalink / raw) In article <3kaksj$iur@isnews.calpoly.edu>, Bill Brooks <wbrooks@hertz.elee.calpoly.edu> wrote: > */ > if (strchr(mapname,'/')) { > strcpy(conf,getenv("PATH_TRANSLATED")); > goto openconf; > } > > if ((fp = fopen(CONF_FILE, "r")) == NULL) > servererr(strcat("Couldn't open configuration file:", CONF_FILE)); > > while(!(getline(input,MAXLINE,fp))) { > char confname[MAXLINE]; > if((input[0] == '#') || (!input[0])) > continue; > for(i=0;isname(input[i]) && (input[i] != ':');i++) > confname[i] = input[i]; > confname[i] = '\0'; > if(!strcmp(confname,mapname)) > goto found; > } >----------------------- end paste --------------------------- >In the rich tradition of discussing good software engineering practices in >c.l.a(regardless of language) I'll ask: is this good coding style? >Keep in mind that this code was written under the auspices of one of >the top 5 schools in CS in the United States. > At the risk of exposing myself as some sort of heretic, the above code example looks perfectly "normal" to me. That's one of the nasty little problems about C, it makes "dense" code "normal". Some may claim that the above style isn't "industrial quality" C code, but that's not been my observation -- I've seen MUCH worse. -- Frustrated with C, C++, Pascal, Fortran? Ada95 _might_ be for you! For all sorts of interesting Ada95 tidbits, run the command: "finger dweller@starbase.neosoft.com | more" (or e-mail with "finger" as subj.) if u cn rd ths, u r gd enuf to chg to Ada :-) ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-19 22:06 ` David Weller @ 1995-03-23 15:05 ` Theodore Dennison 1995-03-24 10:26 ` Fred J. McCall 1995-03-29 0:00 ` Robert I. Eachus ` (2 subsequent siblings) 3 siblings, 1 reply; 76+ messages in thread From: Theodore Dennison @ 1995-03-23 15:05 UTC (permalink / raw) David Weller <dweller@Starbase.NeoSoft.COM> > In article <3kaksj$iur@isnews.calpoly.edu>, > Bill Brooks <wbrooks@hertz.elee.calpoly.edu> wrote: > > while(!(getline(input,MAXLINE,fp))) { > > char confname[MAXLINE]; > > if((input[0] == '#') || (!input[0])) > > continue; > > for(i=0;isname(input[i]) && (input[i] != ':');i++) > > confname[i] = input[i]; > > confname[i] = '\0'; > > if(!strcmp(confname,mapname)) > > goto found; > > } > >In the rich tradition of discussing good software engineering practices in > >c.l.a(regardless of language) I'll ask: is this good coding style? > >Keep in mind that this code was written under the auspices of one of > >the top 5 schools in CS in the United States. > At the risk of exposing myself as some sort of heretic, the above > code example looks perfectly "normal" to me. That's one of the nasty > little problems about C, it makes "dense" code "normal". Some may I think the problem he has with this (at least the problem I have with it) is not that it dense, or even that it is C. It think the problem is the "goto" statements. (At least, that's my problem with it). Now, I too have seen some bad C code in my time. But this is the first I have EVER seen anyone actually use a "goto". In a language with a good selection of looping constructs like C, there is NO excuse for this. (Well, perhaps stupidity...) There, That ought to get the flames going! T.E.D. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-23 15:05 ` Theodore Dennison @ 1995-03-24 10:26 ` Fred J. McCall 1995-03-27 9:50 ` Robb Nebbe 1995-03-27 14:24 ` Should internet support software be written in Ada? Theodore Dennison 0 siblings, 2 replies; 76+ messages in thread From: Fred J. McCall @ 1995-03-24 10:26 UTC (permalink / raw) In article <3ks2o3$bab@theopolis.orl.mmc.com> Theodore Dennison <dennison@escmail.orl.mmc.com> writes: >I think the problem he has with this (at least the problem I have with it) >is not that it dense, or even that it is C. It think the problem is the >"goto" statements. (At least, that's my problem with it). I'd suggest you don't know enough about the code in question to make that kind of judgement. >Now, I too have seen some bad C code in my time. But this is the first I have >EVER seen anyone actually use a "goto". In a language with a good selection of >looping constructs like C, there is NO excuse for this. (Well, perhaps >stupidity...) T'would seem that this commodity is actually on your part. Depending on the application and the structure of the problem, there are times when 'goto' is the appropriate solution. This sort of 'structured programming' bigotry is merely silly and is the sort of thing that leads to code obfuscated by numerous loops, tests, and unnecessary control variables. >There, That ought to get the flames going! Hope you're happy now. Don't bother to reply. The very comment convinces me you don't know enough to have a valid opinion. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-24 10:26 ` Fred J. McCall @ 1995-03-27 9:50 ` Robb Nebbe 1995-03-27 19:43 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Robert I. Eachus 1995-03-27 14:24 ` Should internet support software be written in Ada? Theodore Dennison 1 sibling, 1 reply; 76+ messages in thread From: Robb Nebbe @ 1995-03-27 9:50 UTC (permalink / raw) In article <3ks2o3$bab@theopolis.orl.mmc.com> Theodore Dennison <dennison@escmail.orl.mmc.com> writes: ... >Now, I too have seen some bad C code in my time. But this is the first I have >EVER seen anyone actually use a "goto". In a language with a good selection of >looping constructs like C, there is NO excuse for this. (Well, perhaps >stupidity...) As a control structure a goto provides something that the "structured" control structures do not provide: a permanent transfer of control. Loops, and subprogram calls represent a temporary transfer of control. Now a permanent transfer of control is almost never what you want. The only use I have found is in implementing state machines but even then a goto is not always the best solution. If you need access to state information then you should probably not use gotos. Fred McCall is probably correct in pointing out that we don't really have enough information in the code fragment to judge is the use of gotos was appropriate or not. However, I'm more than a little suspicious when I see code like that. Robb Nebbe ^ permalink raw reply [flat|nested] 76+ messages in thread
* State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-03-27 9:50 ` Robb Nebbe @ 1995-03-27 19:43 ` Robert I. Eachus 1995-03-27 23:14 ` Arthur Evans Jr 1995-03-29 0:00 ` Dan 0 siblings, 2 replies; 76+ messages in thread From: Robert I. Eachus @ 1995-03-27 19:43 UTC (permalink / raw) In article <1995Mar27.113400@di.epfl.ch> Robb.Nebbe@di.epfl.ch (Robb Nebbe) writes: > Now a permanent transfer of control is almost never what you want. The > only use I have found is in implementing state machines but even then > a goto is not always the best solution. If you need access to state > information then you should probably not use gotos. The only goto's I have ever used in Ada, PL/I, Algol, etc. have been either in compiler testing or in state machines. (The former is, of course, no reason to include them in a language.) So AFAIK, the only legitimate use of gotos are in state machines. Of course, compiler builders are among the most prolific users and builders of state machines, so compiler builders want to retain gotos. The question is does that justify their inclusion in modern programming languages? My guess is that the answer is no, but that it is a close call. However, the cost to implement gotos is small, and compiler writers will always voluteer to pay it. -- Robert I. Eachus with Standard_Disclaimer; use Standard_Disclaimer; function Message (Text: in Clever_Ideas) return Better_Ideas is... ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-03-27 19:43 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Robert I. Eachus @ 1995-03-27 23:14 ` Arthur Evans Jr 1995-03-29 0:00 ` Dan 1 sibling, 0 replies; 76+ messages in thread From: Arthur Evans Jr @ 1995-03-27 23:14 UTC (permalink / raw) In article <EACHUS.95Mar27144321@spectre.mitre.org>, eachus@spectre.mitre.org (Robert I. Eachus) wrote: > The only goto's I have ever used in Ada, PL/I, Algol, etc. have > been either in compiler testing or in state machines. (The former is, > of course, no reason to include them in a language.) So AFAIK, the > only legitimate use of gotos are in state machines. Another use is in code that is generated by a tool, where often it is easier to generate a goto than to write code that accomplishes the task some other way. A general truism: It is OK for a tool to generate code that you woyld fire a programmer for writing. Art Evans Arthur Evans Jr, PhD Phone: 412-963-0839 Ada Consulting FAX: 412-963-0927 461 Fairview Road Pittsburgh PA 15238-1933 evans@evans.pgh.pa.us ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-03-27 19:43 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Robert I. Eachus 1995-03-27 23:14 ` Arthur Evans Jr @ 1995-03-29 0:00 ` Dan 1995-04-01 0:00 ` Mike White 1 sibling, 1 reply; 76+ messages in thread From: Dan @ 1995-03-29 0:00 UTC (permalink / raw) In article <EACHUS.95Mar27144321@spectre.mitre.org>, eachus@spectre.mitre.org says... > > The only goto's I have ever used in Ada, PL/I, Algol, etc. have >been either in compiler testing or in state machines. (The former is, >of course, no reason to include them in a language.) So AFAIK, the >only legitimate use of gotos are in state machines. > > Of course, compiler builders are among the most prolific users and >builders of state machines, so compiler builders want to retain gotos. >The question is does that justify their inclusion in modern >programming languages? My guess is that the answer is no, but that it >is a close call. However, the cost to implement gotos is small, and >compiler writers will always voluteer to pay it. > > Although I can appreciate the "goto" argument for conversion tools and (maybe) compilers, most of my embedded applications include at least one state machine, and I've never had to use the goto construct. Perhaps my state machines aren't terribly complex...the toughest one I've done involves two separate state machines to implement X.25 layer 2 (HDLC) and a modified version of X.25 layer 3. I've never built a compiler, so I really can't compare the levels of complexity. Each of the X.25 state machines are (basically) simple tasks containing one main loop enveloping a (huge) case construct. I've always believed this to be the best mechanism to implement these particular state machines, but I'm always open to new ideas. Finally, although the cost to implement gotos may be small (to a compiler manufacturer), the cost to MAINTAIN code with gotos (to a software maintainer) can be enormous. I've done my time in maintenance and development of large FORTRAN (IV and 77) systems, and languages like Ada are a Godsend to me... Dan Kurfis ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-03-29 0:00 ` Dan @ 1995-04-01 0:00 ` Mike White 1995-04-04 0:00 ` Robert Dewar 0 siblings, 1 reply; 76+ messages in thread From: Mike White @ 1995-04-01 0:00 UTC (permalink / raw) DanKurfis wrote: : In article <EACHUS.95Mar27144321@spectre.mitre.org>, : eachus@spectre.mitre.org says... [deleted] : >of course, no reason to include them in a language.) So AFAIK, the : >only legitimate use of gotos are in state machines. [more snipped] : (basically) simple tasks containing one main loop enveloping a (huge) case : construct. I've always believed this to be the best mechanism to implement : these particular state machines, but I'm always open to new ideas. I'd agree. The argument might be made that using a case construct results in slower code, but in fact, a case would only be a comparison and a jump slower than a goto once compiled. The resulting code, however, is more structured and maintainable, IMO. -- *************************************************************************** * Michael White * "Man is a biped without feathers." * * cons116@titan.ucs.umass.edu * -Plato * *************************************************************************** ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-01 0:00 ` Mike White @ 1995-04-04 0:00 ` Robert Dewar 1995-04-06 0:00 ` Theodore Dennison 1995-04-07 0:00 ` Mike White 0 siblings, 2 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-04 0:00 UTC (permalink / raw) OK, I promised myself not to get into this silly goto discussion (having already gone around in it once on comp.lang.cobol). Here is the basic issue with finite state machines. A normal picture of a finite state machine is a spaghetti diagram with circles for states and arrows for transitions. Little gobs of code for the circles, and gotos for the arrows, is a very natural representation. it has exactly the same structure as the original pictorial diagram. For me, the case statement is just a little removed from the motivating diagram, so I find the goto structure clearer. I have often taken polls on this issue in my graduate classes, and I usually find the class divided. OK, that's reasonable, both approaches are certainly acceptable, and obviously have equivalent structure, it is a matter of aesthetics which you prefer. What seems peculiar to me is people who are SURE that the goto solution is somehow less maintainable and less structured. That seems silly to me. I have seen plenty of junk code which strenuously avoids gotos, and pleny of very easily maintained nicely strcutured code that uses gotos. Sure, we all know that gotos are generally to be avoided, like unchecked conversion. However, a rule that says NEVER EVER USE A GOTO is as silly as a rule that says NEVER EVER USE UNCHECKED CONVERSION. People like simple rules. Some programmers are so incompetent that they can only be trusted to work under simple absolute rules. My rule is also simple: get rid of incompetent programmers. Please be clear, I am not saying that anyone who completely avoids gotos is incompetenmt, not at all. I am saying that it is wrong to think that it is appropriate to visit this absolute rule on competent programmers. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-04 0:00 ` Robert Dewar @ 1995-04-06 0:00 ` Theodore Dennison 1995-04-06 0:00 ` Norman H. Cohen ` (2 more replies) 1995-04-07 0:00 ` Mike White 1 sibling, 3 replies; 76+ messages in thread From: Theodore Dennison @ 1995-04-06 0:00 UTC (permalink / raw) dewar@cs.nyu.edu (Robert Dewar) wrote: >Here is the basic issue with finite state machines. A normal picture >of a finite state machine is a spaghetti diagram with circles for >states and arrows for transitions. Which is why people today tend to design using structure charts. >Please be clear, I am not saying that anyone who completely avoids >gotos is incompetenmt, not at all. I am saying that it is wrong to think >that it is appropriate to visit this absolute rule on competent >programmers. I have now worked under 3 different Ada coding standards. Every one of them had a "no goto's" rule. Since I'm currently editing our next coding standard, perhaps someone could suggest a replacement rule? It should be very specific about what allowable and unallowable goto's are. We need something that our software quality folks can enforce. The rule can make NO assumptions about the competency of the programmer, as we won't find out the truth on that matter until it is too late. T.E.D. (structured programming mafioso) ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-06 0:00 ` Theodore Dennison @ 1995-04-06 0:00 ` Norman H. Cohen 1995-04-07 0:00 ` Robert Dewar 1995-04-07 0:00 ` Tucker Taft 2 siblings, 0 replies; 76+ messages in thread From: Norman H. Cohen @ 1995-04-06 0:00 UTC (permalink / raw) In article <3m0nv5$67l@theopolis.orl.mmc.com>, Theodore Dennison <dennison@escmail.orl.mmc.com> writes: |> I have now worked under 3 different Ada coding standards. Every one |> of them had a "no goto's" rule. Since I'm currently editing our next |> coding standard, perhaps someone could suggest a replacement rule? Throughout your coding standard, change all occurrences of "rule" to "guideline" and all occurrences of "shall" to "shall generally". Once these global changes are made, no further local changes are needed for your treatment of gotos. Here's an example to ponder: Consider the declarations type Node_Type; type Tree_Type is access Node_Type; type Node_Type is record Count : Natural := 0; Left, Right : Tree_Type; end record; type Bit_Vector_Type is array (Natural range <>) of Boolean; type Bit_Vector_Pointer_Type is access Bit_Vector_Type; Root : Tree_Type; BV : Bit_Vector_Pointer_Type; BV points to a bit vector describing a path (False = left, True = right) through the tree pointed to by Root. We are counting the number of times a given bit vector is encountered in the Count component of the corresponding tree node. Root starts out pointing to a tree consisting only of a root node, and new nodes are added to the tree as needed. The loop below has three exits, and the actions appropriate when one of the exits is taken is different from the actions appropriate when the other two are taken, so a goto comes in handy. Here's the code: Node := Root; Bit := BV'First; loop if Bit > BV'Last then goto Increment; end if; if BV(Bit) then if Node.Left = null then Node.Left := new Node; Node := Node.Left; exit; else Node := Node.Left; end if; else if Node.Right = null then Node.Right := new Node; Node := Node.Right; exit; else Node := Node.Right; end if; end if; Bit := Bit + 1; end loop; -- We've reached a leaf. Read the rest of BV.all while extending -- the tree along the corresponding path only. for I in Bit+1 .. BV'Last loop if BV(I) then Node.Left := new Node; Node := Node.Left; else Node.Right := new Node; Node := Node.Right; end if; end loop; <<Increment>> Node.Count := Node.Count + 1; Knuth's article in the December 1974 Computing Surveys is still the best discussion I've ever seen of the goto issue. It ought to be required reading early on in any Comp. Sci. curriculum. -- Norman H. Cohen ncohen@watson.ibm.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-06 0:00 ` Theodore Dennison 1995-04-06 0:00 ` Norman H. Cohen @ 1995-04-07 0:00 ` Robert Dewar 1995-04-07 0:00 ` Tucker Taft 2 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-07 0:00 UTC (permalink / raw) T.E.D. asks a difficult question. He wants an absolute set of coding rules. But with regard to GOTO's no absolute set of rules is likely to be a good choice. Probably any formalized set of coding standards should say GOTO's are not allowed. I am worried that if you try to codify the conditions under which GOTO's are reasonable, you will create a backdoor for incompetent programmers to commit crimes against Ada. Of course incompetent programmers will commit such crimes in any case, regardless of standards. Still ... The real point is that any usable set of coding standards must have some flexibility. You get a similar problem trying to describe when the use of unchecked conversion is OK. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-06 0:00 ` Theodore Dennison 1995-04-06 0:00 ` Norman H. Cohen 1995-04-07 0:00 ` Robert Dewar @ 1995-04-07 0:00 ` Tucker Taft 2 siblings, 0 replies; 76+ messages in thread From: Tucker Taft @ 1995-04-07 0:00 UTC (permalink / raw) Theodore Dennison (dennison@escmail.orl.mmc.com) wrote: : dewar@cs.nyu.edu (Robert Dewar) wrote: : >Here is the basic issue with finite state machines. A normal picture : >of a finite state machine is a spaghetti diagram with circles for : >states and arrows for transitions. One reason to prefer case statements over gotos for implementing a finite state machine is that there is no danger of forgetting the "goto" at the "end" of a state's code. Using gotos instead of a "case" statement opens up the programmer to the same kind of bug as the notorious "missing break" in C/C++ switch statements. You might just flow through to the state that happened to follow in the text of the program, without intending to. E.g.: goto Initial_State; <<state_1>> blah; blah; -- oops, I forgot the goto. <<state_2>> ... Versus: State : State_Enum := Initial_State; Next_State : State_Enum; begin loop Next_State := Uninitialized_State; case State is when State_1 => blah; blah; -- oops, I forgot to set Next_State when State_2 => ... end case; if Next_State = Uninitialized_State then Put_Line("Next_State not set"); Put_Line("Previous state is " & State_Enum'Image(State)); raise Program_Error; end if; State := Next_State; -- Advance to next state end loop; Of course, you could also see the goto-based approach's capability of "flowing through" as a nice opportunity for optimization (that is presumably why "break;" is not the default in C/C++ switch statements). However, I believe few would argue at this point with 20/20 hindsight (including the most die-hard C programmer), that the C/C++ default of "fall through" between switch alternatives was the right choice. : Which is why people today tend to design using structure charts. : >Please be clear, I am not saying that anyone who completely avoids : >gotos is incompetenmt, not at all. I am saying that it is wrong to think : >that it is appropriate to visit this absolute rule on competent : >programmers. : I have now worked under 3 different Ada coding standards. Every one : of them had a "no goto's" rule. Since I'm currently editing our next : coding standard, perhaps someone could suggest a replacement rule? It : should be very specific about what allowable and unallowable goto's : are. We need something that our software quality folks can enforce. : The rule can make NO assumptions about the competency of the programmer, : as we won't find out the truth on that matter until it is too late. Here is a half-serious ;-} suggestion: How about requiring the programmer to write a short paragraph in the comments, on why the goto was the most appropriate solution for the given problem? Require that the paragraph be no less than 20 words, and no more than 100 words long. The net effect would be to create a sufficient incentive that the programmer would have to think hard before using a goto. : T.E.D. (structured programming mafioso) -Tucker Taft stt@inmet.com Intermetrics, Inc. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-04 0:00 ` Robert Dewar 1995-04-06 0:00 ` Theodore Dennison @ 1995-04-07 0:00 ` Mike White [not found] ` <3ma7rt$smt@kaiwan009.kaiwan.com> 1 sibling, 1 reply; 76+ messages in thread From: Mike White @ 1995-04-07 0:00 UTC (permalink / raw) Robert Dewar (dewar@cs.nyu.edu) wrote: : OK, I promised myself not to get into this silly goto discussion (having : already gone around in it once on comp.lang.cobol). : Here is the basic issue with finite state machines. A normal picture : of a finite state machine is a spaghetti diagram with circles for : states and arrows for transitions. : Little gobs of code for the circles, and gotos for the arrows, is a very : natural representation. it has exactly the same structure as the original : pictorial diagram. : For me, the case statement is just a little removed from the motivating : diagram, so I find the goto structure clearer. I have often taken polls : on this issue in my graduate classes, and I usually find the class divided. The goto structure certainly reflects the FSM diagram in an intuitive manner. However, many of us simply loathe using it - I haven't used a goto in a program since I last used BASIC: probably 6 or 7 years ago. It HAS been ingrained in all coursework I have had. One possibility for making the case structure more reflective of the machine it is based on is by having a procedure something like GoFromStateToState (current_state, state_of_bliss) or even a function like current_state = GotoState (state_of_bliss) which simply sets the value of current_state to state_of_bliss. This does not change the fact that it is still a case structure, but it might make the code more closely model, at least for a maintainer, the FSM it is implementing. [cut] : People like simple rules. Some programmers are so incompetent that they : can only be trusted to work under simple absolute rules. My rule is : also simple: get rid of incompetent programmers. This almost sounds like a typical argument against Ada from the C people! :) (The part about sticking to the rules, not programmer competence...) Adhering to fairly simple rules is, IMO, essential for maintainability. They should not be absolute, but nearly, as most problems _can_ be solved without using tricks and without making the code particularly contrived. As I see it, the ability to find elegant solutions while adhering to fairly strict rules is what defines a competent programmer. -- *************************************************************************** * Michael White * "Man is a biped without feathers." * * cons116@titan.ucs.umass.edu * -Plato * *************************************************************************** ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <3ma7rt$smt@kaiwan009.kaiwan.com>]
[parent not found: <dewar.797514490@gnat>]
[parent not found: <3meunj$66u@felix.seas.gwu.edu>]
* Re: CS teachers who can't code their way outta a paper bag [not found] ` <3meunj$66u@felix.seas.gwu.edu> @ 1995-04-20 0:00 ` Richard A. O'Keefe 0 siblings, 0 replies; 76+ messages in thread From: Richard A. O'Keefe @ 1995-04-20 0:00 UTC (permalink / raw) mfeldman@seas.gwu.edu (Michael Feldman) writes: >What's the equivalent in software? Are our industry colleagues >willing to let us have the source code for _good_ industrial-strength >projects, so that we can our students can explore it? I don't mean the >isolated components and "assets" of varying quality tossed into the PAL, >I mean _real_ stuff. I am currently negotiating to get access to the source code for a program called "CC" (no, it isn't a C compiler) to use in an SE project. It's a real existing program with a real user base and a real performance problem that I hope we may be able to do something about. I expect that I and my students will learn a lot from working with it, even though it is moderately small. I am *really* looking forward to having real code for my students to work with. I know my other colleagues at RMIT feel the same way and are also looking for real projects in their respective areas. -- "The complex-type shall be a simple-type." ISO 10206:1991 (Extended Pascal) Richard A. O'Keefe; http://www.cs.rmit.edu.au/~ok; RMIT Comp.Sci. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-24 10:26 ` Fred J. McCall 1995-03-27 9:50 ` Robb Nebbe @ 1995-03-27 14:24 ` Theodore Dennison 1995-03-28 0:00 ` Robert Dewar 1995-03-28 9:32 ` Fred J. McCall 1 sibling, 2 replies; 76+ messages in thread From: Theodore Dennison @ 1995-03-27 14:24 UTC (permalink / raw) Fred J. McCall <fjm@ti.com> writes > In article <3ks2o3$bab@theopolis.orl.mmc.com> Theodore Dennison <dennison@escmail.orl.mmc.com> writes: > >Now, I too have seen some bad C code in my time. But this is the first I have > >EVER seen anyone actually use a "goto". In a language with a good selection of > >looping constructs like C, there is NO excuse for this. (Well, perhaps > >stupidity...) > > T'would seem that this commodity is actually on your part. Depending on the > application and the structure of the problem, there are times when 'goto' is > the appropriate solution. This sort of 'structured programming' bigotry is > merely silly and is the sort of thing that leads to code obfuscated by > numerous loops, tests, and unnecessary control variables. "Structured Programming Bigotry"? Are you being serious? Well, in case you are, I'm now curious. At what times is a "goto" an appropriate solution? The best excuse I ever heard was for simulating exception handling in a language that didn't support it. I'm sorry if I'm taking sarcasm seriously, but I didn't see any smileys. > > >There, That ought to get the flames going! > > Hope you're happy now. Don't bother to reply. The very comment convinces me > you don't know enough to have a valid opinion. Oooh! Looks like I was right. T.E.D. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-27 14:24 ` Should internet support software be written in Ada? Theodore Dennison @ 1995-03-28 0:00 ` Robert Dewar 1995-03-28 9:32 ` Fred J. McCall 1 sibling, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-03-28 0:00 UTC (permalink / raw) Hello, looks like a goto debate is about to start. It always surprises me how many people react so defensively at the idea of a goto. Most peculiar. Of course gotos are very rarely used. Of course they are sometimes useful and appropriate. In my experience it is a total waste of time to try to convnice people of this if they are dead set against gotos, it's like trying to argue religeon. For me, if someone doesn't see that gotos are sometimes useful, fine, they are entitled to their [peculiar] opinion, and why should I bother to try to persaude them otherwise. No smileys here, none needed really, well maybe one for this last sentence itself :-) If you want to save yourself the troubvle of reading a long thread on this, you could look at the long thread that just completed in comp.lang.cobol on this very topic (of course on that newsgroup there are also people who are convinced that mainframes will be around for ever :-) ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-27 14:24 ` Should internet support software be written in Ada? Theodore Dennison 1995-03-28 0:00 ` Robert Dewar @ 1995-03-28 9:32 ` Fred J. McCall 1995-03-29 0:00 ` Theodore Dennison 1 sibling, 1 reply; 76+ messages in thread From: Fred J. McCall @ 1995-03-28 9:32 UTC (permalink / raw) In article <3l6hra$h05@theopolis.orl.mmc.com> Theodore Dennison <dennison@escmail.orl.mmc.com> writes: >Fred J. McCall <fjm@ti.com> writes >> In article <3ks2o3$bab@theopolis.orl.mmc.com> Theodore Dennison <dennison@escmail.orl.mmc.com> writes: >> >Now, I too have seen some bad C code in my time. But this is the first I have >> >EVER seen anyone actually use a "goto". In a language with a good selection of >> >looping constructs like C, there is NO excuse for this. (Well, perhaps >> >stupidity...) >> >> T'would seem that this commodity is actually on your part. Depending on the >> application and the structure of the problem, there are times when 'goto' is >> the appropriate solution. This sort of 'structured programming' bigotry is >> merely silly and is the sort of thing that leads to code obfuscated by >> numerous loops, tests, and unnecessary control variables. >"Structured Programming Bigotry"? Are you being serious? Yes. >Well, in case you are, I'm now curious. At what times is a "goto" an >appropriate solution? The best excuse I ever heard was for simulating exception >handling in a language that didn't support it. Any time the code is 'cleaner' with it than without it. This is often the case for things like state machines and dispatchers. By all means, though, if you don't have the judgement to be able to tell, you probably should never use it. >I'm sorry if I'm taking sarcasm seriously, but I didn't see any smileys. There weren't any. Any time you think you can unequivocably say that 'construct X is bad and should never be used', you are almost certainly wrong. This is *EXACTLY* the sort of thinking all too many 'structured programming bigots' inflict on the people around them. >> >> >There, That ought to get the flames going! >> >> Hope you're happy now. Don't bother to reply. The very comment convinces me >> you don't know enough to have a valid opinion. >Oooh! Looks like I was right. Wrong twice. One more strike and you're out. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-28 9:32 ` Fred J. McCall @ 1995-03-29 0:00 ` Theodore Dennison 0 siblings, 0 replies; 76+ messages in thread From: Theodore Dennison @ 1995-03-29 0:00 UTC (permalink / raw) Fred J. McCall <fjm@ti.com> writes > >Well, in case you are, I'm now curious. At what times is a "goto" an > >appropriate solution? The best excuse I ever heard was for simulating > Any time the code is 'cleaner' with it than without it. This is often the > case for things like state machines and dispatchers. By all means, though, if > you don't have the judgement to be able to tell, you probably should never use > it. > Could you be more specific than "state machines"? Any algorithm can be expressed as a state machine (I believe there is actually a theorem to this effect, but it's been a while since college). I have written a dispatcher before. It seemed clean enough as a loop enclosing a case statement. I don't think goto's would have made it clearer. T.E.D. (structured programming bigot) ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-19 22:06 ` David Weller 1995-03-23 15:05 ` Theodore Dennison @ 1995-03-29 0:00 ` Robert I. Eachus 1995-03-31 0:00 ` Theodore Dennison 1995-04-05 0:00 ` Wes Groleau 1995-04-07 0:00 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Wes Groleau 3 siblings, 1 reply; 76+ messages in thread From: Robert I. Eachus @ 1995-03-29 0:00 UTC (permalink / raw) In article <3lbp1k$jij@theopolis.orl.mmc.com> Theodore Dennison <dennison@escmail.orl.mmc.com> writes: > Could you be more specific than "state machines"? Any algorithm > can be expressed as a state machine (I believe there is actually a > theorem to this effect, but it's been a while since college). > I have written a dispatcher before. It seemed clean enough as a > loop enclosing a case statement. I don't think goto's would have > made it clearer. A simple state machine can be expressed as a case statement in a loop. A more complex state machine will often have several selection criteria, or may have states for which the "normal" method of choosing the next state do not apply. (The canonical example of these is error recovery.) In such a state machine you can keep adding flags and tests to keep the original structure intact, but a much better approach is to say goto when you know where to go next. It is much easier to understand, and, surprise, surprise, it is a lot easier to maintain. Let me give you a simple example. A parser generator generated tables which were headers followed by lists of triples: (symbol, action, next state). Since many lists only differed from the a similar state because they had one or two added triples, we put in an optimization where some table headers indicated that if you didn't find a match in this table you should go to some other table and try there. (There are the magic words again.) Now I could have written the parser with a loop of the form: while In_Continue_Table loop --search table... end loop; But that code would be totally misleading. What I wrote was: <<Try_Again>> case Table.Kind is ... when Continue_Table => if S /= Table.Entries(1) then Table := Table.Continuation; goto Try_Again; else -- process a match. end if; This makes it much clearer that you go back to the "top" of the case statement only in specific failure cases. Another example in the same parser involved "panic mode" recovery. If a neat clean correction can be found that allows the compiler to continue can be found, make it and go on. If not, you want to go back to a consistant state and proceed from there. Again if hand-waving description uses go to, the proper implementation probably uses gotos. In this case the reason for using goto was that the proper continuation point depended on the type of error detected. I could have written this in Ada with several exceptions, several block statements, several loops, etc. Or I could, and did just use gotos with appropriate labels so that the code was understandable. Now in both these cases, my description admitted that either one could have been implemented without gotos. As it happened, since both of these were in the same code, and the artificially created nested scopes would not have matched, one or the other had to be done with gotos. (Or you could use a number of artificial state variables, etc., etc., like you learned in classes on computability theory. But not in anything I'm going to maintain!) -- Robert I. Eachus with Standard_Disclaimer; use Standard_Disclaimer; function Message (Text: in Clever_Ideas) return Better_Ideas is... ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-29 0:00 ` Robert I. Eachus @ 1995-03-31 0:00 ` Theodore Dennison 0 siblings, 0 replies; 76+ messages in thread From: Theodore Dennison @ 1995-03-31 0:00 UTC (permalink / raw) eachus@spectre.mitre.org (Robert I. Eachus) wrote: > A simple state machine can be expressed as a case statement in a >loop. A more complex state machine will often have several selection >criteria, or may have states for which the "normal" method of choosing >the next state do not apply. (The canonical example of these is error >recovery.) > > In such a state machine you can keep adding flags and tests to >keep the original structure intact, but a much better approach is to >say goto when you know where to go next. It is much easier to >understand, and, surprise, surprise, it is a lot easier to maintain. > Thank you for your explanation, and your example. In the dispatcher I wrote, I did have a similar problem. I ended up handling it by performing all the error checking BEFORE the dispatching algorithm got called. I also set up all of the dispatching conditions beforehand in boolean expressions (with judicious use of short-circuts and boolean parsing functions). I have to admit that the code for those parts did get kinda ugly. But it made the dispatcher itself relatively simple. It also had the drawback that some parsing might be done more than once. I can see where this would be unacceptable for compiler writers who are worried about benchmark performance. I guess I can see where you guys are comming from now. However, I think your cure may be worse than the disease. T.E.D. p.s. Ignore me, I`m a "structured programming bigot" ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-19 22:06 ` David Weller 1995-03-23 15:05 ` Theodore Dennison 1995-03-29 0:00 ` Robert I. Eachus @ 1995-04-05 0:00 ` Wes Groleau 1995-04-07 0:00 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Wes Groleau 3 siblings, 0 replies; 76+ messages in thread From: Wes Groleau @ 1995-04-05 0:00 UTC (permalink / raw) >Hello, looks like a goto debate is about to start. It always surprises me >....... Hey, well Dijkstra said 'goto' is bad, so we sheep had better get in line! There are always those that jump on every new bandwagon with no comprehnsion of the tune the band is playing. What's the difference between the 'goto FOUND_CONFIG' in the example that started this and " exit FIND_CONFIG" inin Ada? compare also "raise EXCEP" and " goto <<EXCEP_HANDLER>>" pardon my syntax, I'm ... ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-03-19 22:06 ` David Weller ` (2 preceding siblings ...) 1995-04-05 0:00 ` Wes Groleau @ 1995-04-07 0:00 ` Wes Groleau 1995-04-07 0:00 ` Robert Firth 3 siblings, 1 reply; 76+ messages in thread From: Wes Groleau @ 1995-04-07 0:00 UTC (permalink / raw) In a previous article, dennison@escmail.orl.mmc.com (Theodore Dennison) says: >I have now worked under 3 different Ada coding standards. Every one >of them had a "no goto's" rule. Since I'm currently editing our next >coding standard, perhaps someone could suggest a replacement rule? X.Y.Z.1 A goto statement shall NOT be used where another legal Ada construct is available for the same effect. Example: REJECT: OK: ... ... goto GOT_IT; exit GET_IT; end loop GET_IT; end loop GET_IT; <<GOT_IT>> X.Y.Z.2 When a goto statement is coded which is NOT in violation of X.Y.Z.1, a review meeting with at least one other programmer of equivalent experience and at least one programmer with ____ years Ada experience shall be held within five working days to determine whether the use is justified or whether the associated units should be redesigned. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-07 0:00 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Wes Groleau @ 1995-04-07 0:00 ` Robert Firth [not found] ` <D6qyv0.6Jv@nntpa.cb.att.com> 0 siblings, 1 reply; 76+ messages in thread From: Robert Firth @ 1995-04-07 0:00 UTC (permalink / raw) In article <3m3j73$php@tali.hsc.colorado.edu> bl884@freenet.HSC.Colorado.EDU (Wes Groleau) writes: >X.Y.Z.1 A goto statement shall NOT be used where another legal Ada construct >is available for the same effect. X.Y.Z.2: a goto statement shall not be used merely to avoid the replication of code. Example: when '+' => sign := positive; goto get_rest_of_number; when '-' => sign := negative; goto get_rest_of_number; ... ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <D6qyv0.6Jv@nntpa.cb.att.com>]
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) [not found] ` <D6qyv0.6Jv@nntpa.cb.att.com> @ 1995-04-19 0:00 ` Fergus Henderson 1995-04-19 0:00 ` Fred J. McCall 0 siblings, 1 reply; 76+ messages in thread From: Fergus Henderson @ 1995-04-19 0:00 UTC (permalink / raw) ka@socrates.hr.att.com (Kenneth Almquist) writes: >firth@sei.cmu.edu (Robert Firth) writes: >> X.Y.Z.2: a goto statement shall not be used merely to avoid the >> replication of code. Example: >> >> when '+' => >> sign := positive; >> goto get_rest_of_number; >> when '-' => >> sign := negative; >> goto get_rest_of_number; >> ... > >No, No, No, No, No!!!!!!! > >Sorry if this is somewhat heated, but every time you replicate code you are >creating a potential maintainance headache that *somebody* is going to have >to deal with. The alternative should not be to replicate the code, it should be to put the common code into a procedure or function. when '+' => get_rest_of_number(sign => positive); when '-' => get_rest_of_number(sign => positive); -- Fergus Henderson | As practiced by computer science, the study of fjh@cs.mu.oz.au | programming is an unholy mixture of mathematics, http://www.cs.mu.oz.au/~fjh | literary criticism, and folklore. - B. A. Sheil ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-19 0:00 ` Fergus Henderson @ 1995-04-19 0:00 ` Fred J. McCall 1995-04-19 0:00 ` George Haddad ` (3 more replies) 0 siblings, 4 replies; 76+ messages in thread From: Fred J. McCall @ 1995-04-19 0:00 UTC (permalink / raw) In article <9511002.21479@mulga.cs.mu.OZ.AU> fjh@munta.cs.mu.OZ.AU (Fergus Henderson) writes: >The alternative should not be to replicate the code, it should >be to put the common code into a procedure or function. And what if the common code is (relatively) large and using a (relatively) large number of the variables used by the procedure that it is already in and needs them to have the values which they have at the point where the 'repeated' code occurs? Presumably you propose writing a function or procedure with 15-20 parameters? I don't consider that particularly good practice. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-19 0:00 ` Fred J. McCall @ 1995-04-19 0:00 ` George Haddad 1995-04-20 0:00 ` Mark A Biggar ` (2 subsequent siblings) 3 siblings, 0 replies; 76+ messages in thread From: George Haddad @ 1995-04-19 0:00 UTC (permalink / raw) In article <fjm.84.000D0007@ti.com>, fjm@ti.com (Fred J. McCall) wrote: > And what if the common code is (relatively) large and using a (relatively) > large number of the variables used by the procedure that it is already in and > needs them to have the values which they have at the point where the > 'repeated' code occurs? Presumably you propose writing a function or > procedure with 15-20 parameters? I don't consider that particularly good > practice. Write a local procedure in the current scope (if the common code is really large, make it "separate"). Then, if necessary for performance, INLINE it. -- I found these opinions on my doorstep, could you please give them a good home? ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-19 0:00 ` Fred J. McCall 1995-04-19 0:00 ` George Haddad @ 1995-04-20 0:00 ` Mark A Biggar 1995-04-20 0:00 ` Bill Winn 1995-04-20 0:00 ` State machines and Goto's (was Re: Sho Brian Hanson 3 siblings, 0 replies; 76+ messages in thread From: Mark A Biggar @ 1995-04-20 0:00 UTC (permalink / raw) In article <fjm.84.000D0007@ti.com> fjm@ti.com (Fred J. McCall) writes: >In article <9511002.21479@mulga.cs.mu.OZ.AU> fjh@munta.cs.mu.OZ.AU (Fergus Henderson) writes: >>The alternative should not be to replicate the code, it should >>be to put the common code into a procedure or function. >And what if the common code is (relatively) large and using a (relatively) >large number of the variables used by the procedure that it is already in and >needs them to have the values which they have at the point where the >'repeated' code occurs? Presumably you propose writing a function or >procedure with 15-20 parameters? I don't consider that particularly good >practice. This may be one of the few times where the nested procedure/function ability of Ada may pay off big time. Usually I never write nested routines, ,they are amost never necesary, but if I had the above postulated situation I probably would use one. -- Mark Biggar mab@wdl.loral.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-19 0:00 ` Fred J. McCall 1995-04-19 0:00 ` George Haddad 1995-04-20 0:00 ` Mark A Biggar @ 1995-04-20 0:00 ` Bill Winn 1995-04-20 0:00 ` Robert Dewar 1995-04-20 0:00 ` State machines and Goto's (was Re: Sho Brian Hanson 3 siblings, 1 reply; 76+ messages in thread From: Bill Winn @ 1995-04-20 0:00 UTC (permalink / raw) In article <fjm.84.000D0007@ti.com>, fjm@ti.com communicates... >And what if the common code is (relatively) large and using a (relatively) >large number of the variables used by the procedure that it is already in and >needs them to have the values which they have at the point where the >'repeated' code occurs? Presumably you propose writing a function or >procedure with 15-20 parameters? I don't consider that particularly good >practice. > > <step on soapbox> If you need to send 15-20 parameters to a function I would say that your function is probably not sufficiently narrow in scope. According to most good software engineering principles that I have seen, a function should do *1* thing, do it well, and move on (thank you Charles Winchester III). Therefore, I would first look at the problem and see if the best abstraction has been choosen. A function with 15-20 paramters has probably not been properly abstracted. For the sake of argument let us assume that one has properly abstracted the problem and found that: (1) 15-20 data are needed for the function; and (2) it makes no sense to split the function into smaller functions (this is a stretch, but stick with me). In this case I would suggest that one could use accessor routines to the needed data, rather than passing all data as parameters. This would: (1) help support encapsulation of the required data elements; (2) avoid nasty interfaces; and (3) avoid global data (my CS degree requires me to say this!). <step off soapbox> Bill Winn Software Engineer - Analysts International Corporation ------------------------------- wjwinn@kocrsv01.delcoelect.com My views do not express the views of anyone except my alter-ego. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Should internet support software be written in Ada?) 1995-04-20 0:00 ` Bill Winn @ 1995-04-20 0:00 ` Robert Dewar 0 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-20 0:00 UTC (permalink / raw) Bill Winn, I am not sure your soapbox is appropriate, it seems like you were triggered by the 15-20 parameters and had not followed the original thread, which had to do with duplicated code from nested conditionals. So we are talking about a section of code referencing 15-20 local variables. That's not so terrible .... In a language with no nested procedures (perhaps with a 1 character name or a 1 character name with some special characters), this can be a real pain. But if you have nested procedures, then this is a good place to use them. I also note that this is a place where some programmers will find it clearer to use a goto (of course other programmers take one look at a goto, and it is like seeing an upside down cross :-) I would certainly prefer the single goto to a junk global procedure with 15-20 parameters! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: State machines and Goto's (was Re: Sho 1995-04-19 0:00 ` Fred J. McCall ` (2 preceding siblings ...) 1995-04-20 0:00 ` Bill Winn @ 1995-04-20 0:00 ` Brian Hanson 3 siblings, 0 replies; 76+ messages in thread From: Brian Hanson @ 1995-04-20 0:00 UTC (permalink / raw) In article 000D0007@ti.com, fjm@ti.com (Fred J. McCall) writes: > In article <9511002.21479@mulga.cs.mu.OZ.AU> fjh@munta.cs.mu.OZ.AU (Fergus Henderson) writes: > > >The alternative should not be to replicate the code, it should > >be to put the common code into a procedure or function. > > And what if the common code is (relatively) large and using a (relatively) > large number of the variables used by the procedure that it is already in and > needs them to have the values which they have at the point where the > 'repeated' code occurs? Presumably you propose writing a function or > procedure with 15-20 parameters? I don't consider that particularly good > practice. Can you say "Nested procedure definition"? -- -- Brian Hanson -- brh@cray.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Should internet support software be written in Ada? 1995-03-17 0:24 Should internet support software be written in Ada? Bill Brooks 1995-03-17 8:47 ` Anthony Shipman 1995-03-19 22:06 ` David Weller @ 1995-03-22 23:08 ` Keith Thompson [not found] ` <dewar.798093453@gnat> ` (4 subsequent siblings) 7 siblings, 0 replies; 76+ messages in thread From: Keith Thompson @ 1995-03-22 23:08 UTC (permalink / raw) Bill Brooks <wbrooks@hertz.elee.calpoly.edu> wrote: > */ > if (strchr(mapname,'/')) { > strcpy(conf,getenv("PATH_TRANSLATED")); > goto openconf; > } > > if ((fp = fopen(CONF_FILE, "r")) == NULL) > servererr(strcat("Couldn't open configuration file:", CONF_FILE)); > > while(!(getline(input,MAXLINE,fp))) { > char confname[MAXLINE]; > if((input[0] == '#') || (!input[0])) > continue; > for(i=0;isname(input[i]) && (input[i] != ':');i++) > confname[i] = input[i]; > confname[i] = '\0'; > if(!strcmp(confname,mapname)) > goto found; > } > ----------------------- end paste --------------------------- > In the rich tradition of discussing good software engineering practices in > c.l.a(regardless of language) I'll ask: is this good coding style? > Keep in mind that this code was written under the auspices of one of > the top 5 schools in CS in the United States. Whether it's good style or not, it's incorrect. The strcat() function modifies its first parameter (more precisely, its first parameter is a pointer and it modifies what it points to). In the statement > servererr(strcat("Couldn't open configuration file:", CONF_FILE)); the first parameter is a string literal. Result: the statement writes the value of CONF_FILE immediately after wherever the compiler decided to store the value for the string literal. As it happens, this is unlikely to cause the program to fail visibly (the line is executed only when the configuration file can't be opened, and the program probably terminates immediately afterward). Perhaps someone who knows where this code came from (I've lost the original article) should notify the authors. -- Keith Thompson (The_Other_Keith) kst@thomsoft.com (kst@alsys.com still works) TeleSoft^H^H^H^H^H^H^H^H Alsys^H^H^H^H^H Thomson Software Products 10251 Vista Sorrento Parkway, Suite 300, San Diego, CA, USA, 92121-2718 That's Keith Thompson *with* a 'p', Thomson Software Products *without* a 'p'. ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <dewar.798093453@gnat>]
* Re: What good is halting prob? [not found] ` <dewar.798093453@gnat> @ 1995-04-20 0:00 ` Max Hailperin 0 siblings, 0 replies; 76+ messages in thread From: Max Hailperin @ 1995-04-20 0:00 UTC (permalink / raw) In article <cppD77EIB.D79@netcom.com> cpp@netcom.com (Robin Rowe) writes: ..., it's still not clear what about the halting problem is actually useful. How can it be used in design? What problems does it help you solve?... The way it is used in design is as a way to help you distinguish between two situations that on the surface look very similar: 1) You're trying to figure out how to program something, and can't figure out how -- everything you try runs into insurmountable obstacles. You start to wonder whether the problem can be solved at all. It turns out it can, you just need to approach it differently. 2) You're trying to figure out how to program something, and can't figure out how -- everything you try runs into insurmountable obstacles. You start to wonder whether the problem can be solved at all. It turns out it can't, you need to find a way to live without a solution -- maybe by accepting some approximation. When you hit that point of doubting whether the problem you're working on is solvable, it is valuable to take some time off from trying to solve it and instead try to prove it unsolvable. If you succeed in your proof, then you know you are in situation 2 and should work on re-defining the problem instead of trying futilely to solve it. If you fail in your proof, you may well have in the course of the failed proof attempt done enough thinking about the problem in different ways to be able to now approach solving it differently and succeed. The way these proofs are usually constructed is by showing that if you could solve the problem at hand, you could use that to solve the halting problem. Hence, since the halting problem is unsolvable, so is the problem at hand. Here's an example; this is a semi-plausible "real-life-ish" scenario; I'm aware its not perfect in this regard, but its the best I could come up with off the top of my head just now, and I hope that it will help convince you that "really real" scenarios might arise: J. Programmer is working on an package for arbitrary-precision calculations. The user is supposed to be able to select any of the result values and request that it be redisplayed to a higher precision, which the user gets to specify. J. Programmer builds an approximation class (where each instance represents some particular number to some particular precision), and gives it a complete set of overloaded operations, so that you can do things like add two approximations and get an approximation. (The precision of the resulting approximation is suitably derived from the precision of the input approximations.) After this is working, J.'s next step is an "arbitrary precision number" class; each instance represents the abstract precision-independent "essence" of a number, and supports an operation which, when given the precision, will return an approximation of that precision. For example, if pi is an instance of this class, you can ask pi for an approximation of itself good to within 10^-2, and get back the approximation that would display as 3.14, or you can ask it for an approximation of itself good to within 10^-5 and get back the approximation that would display as 3.14159, etc. The way this is achieved varies from subclass to subclass; any given subclass of arbitrary precision number needs some way of doing it, but it can vary. J. Programmer none the less can and does supply the abstract super-class with a full complement of arithmetic operators; for example, you can add any two arbitrary precision numbers and get an arbitrary precision sum. The way J. makes this work is that the sum is of a subclass that has two instance variables, one for the augend and one for the addend. It provides an implementation for the "return an approximation of yourself good to this precision" method, namely, it turns around and asks the addend and augend for suitably more precise approximations of themselves than is desired for the sum, and then adds those approximations to get the approximation to the sum. This general strategy works for operations other than addition as well, and J. Programmer is busily buzzing along, picking off operations one by one and implementing them for the general arbitrary precision number class, until one day the == operator (i.e., equality testing) comes to the top of the to-do list. Nothing works. In fact, J. doesn't see any way it could be possible. But, the last time J. loudly declared a programming problem to be "impossible," C. Scientist from down the hall overheard and said "no, it's not impossible, in fact, it's in Knuth." So, remembering this, J. goes down the hall to see C. C. says "yes, this time I think you're right that its impossible -- I bet we can reduce the halting problem to it." The proof goes like this: if you had some procedure (let's call it P) that you wanted to test to see whether it halts, you could encapsulate it into an instance of a new subclass of arbitrary precision number. The way this subclass implements the "return an approximation of yourself to this precision" method is as follows: when asked to return an approximation good to within 10^-n, it simulates execution of P for n steps, or until P terminates, if it terminates in less than n steps. If P terminated in less than n steps, let's say in k steps, then the approximation returned is 10^-k. Otherwise, it is 0. Now, if you had an == operator, you could just check whether this number was == to 0 [or rather, to 0 converted to an arbitrary precision number]. If they are equal, then P doesn't halt. If they aren't equal, then P does halt. So, you've solved the halting problem! So, since that's impossible, it must be impossible to write a general == too. Armed with this knowledge, J. Programmer now can stop trying to implement == for arbitrary precision numbers, and instead work on finding some way to live without them. ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <dewar.798207931@gnat>]
[parent not found: <cppD78ywq.B31@netcom.com>]
[parent not found: <dewar.798240702@gnat>]
* Re: Problems with proofs [not found] ` <dewar.798240702@gnat> @ 1995-04-19 0:00 ` Brian Harvey 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Robin Rowe 2 siblings, 1 reply; 76+ messages in thread From: Brian Harvey @ 1995-04-19 0:00 UTC (permalink / raw) dewar@cs.nyu.edu (Robert Dewar) writes: >but if, like most people, you find that one of the many weak links on the >chain is in incorrect implementation of specifications, then proof of >correctness is one tool in the programmers forge for strengthening this >link. Well then I think they should call it "proof of conformance to specification" rather than "proof of correctness"! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-19 0:00 ` Problems with proofs Brian Harvey @ 1995-04-19 0:00 ` Robert Dewar 0 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-19 0:00 UTC (permalink / raw) Brian says: "Well then I think they should call it "proof of conformance to specification" rather than "proof of correctness"!" Indeed! if this phrase had been used consistently, perhaps a lot of oversell and overexpectation could have been avoided. Anyway, just remember that when you se someone talking about POC they do indeed mean nothing more than POCTS. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs [not found] ` <dewar.798240702@gnat> 1995-04-19 0:00 ` Problems with proofs Brian Harvey @ 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Robin Rowe 2 siblings, 0 replies; 76+ messages in thread From: Robin Rowe @ 1995-04-20 0:00 UTC (permalink / raw) To: dewar@cs.nyu.edu (Robert Dewar) Robert, I mistakenly attributed your post to Steve Tate, and replied to him. Here's the reply I intended to your post. << Nope [to that proofs are based on what appears relevant to a human being to prove], proofs are based on formal specifications of the task at hand. >> So, it's not human beings who decide what belongs in the formal specifications? By the way, please define the term "formal" as you are using it here with regard to specifications. << This [that there is no proof that the proof is equivalent to the code] is based on a misconception, a proof of correctness, if is is any use at all, must have a formal relationship to the code. >> Please define the term "formal" as you are using it here. << Typically assertions in the code are used to guide an actual proof of the correctness of the actual code. Nothing else is useful. >> I'm not clear what you are trying to say here. Are you really saying that the only really useful proofs are those expressed in code? (I think so, too, but this is a radical viewpoint.) << Proofs of correctness must be machine verified to be accepted. >> Please define the term "verified" as you are using it here. << Interfaces to components are part of the axiomatic structure of proven components, and on one side you prove that a component properly handles uses that conform to its interface, and on the other, you prove that the use by a client conforms to this interface. >> This sounds reasonable, and what I expected, too. However, I've been told that valid ranges are often specified arbitrarily. Invalid input is the user's (engineer's) lookout. Have I been misinformed? Is it generally more comprehensive? << I have no idea what you mean by random error. >> Cosmic rays, accidents, etc. << [Proofs take into account hardware failure] if the spec includes this, and they don't if the spec does not. >> Isn't this a pretty loose way to look at proof? Proving that you conformed to a (possibly erroneous) specification sounds a lot less impressive than saying you have a "proof of correctness." In fact, the term seems very misleading since I don't think it is really proven in the mathematical sense nor correct in the engineering sense. << I think you have an idea that a program that is proved correct is guaranteed to work. >> A mind reader you're not. << If you have a 100% track record in implementing code that exactly conforms to its specifications, wonderful! I think proof of correctness won't help, but if, like most people, you find that one of the many weak links on the chain is in incorrect implementation of specifications, then proof of correctness....>> Hmmm, I may have to change my mind about the utility of the halting problem. Implementing code that exactly conforms to its specifications sounds like the halting problem to me. Thanks for the feedback. Good points. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs [not found] ` <dewar.798240702@gnat> 1995-04-19 0:00 ` Problems with proofs Brian Harvey 1995-04-20 0:00 ` Robin Rowe @ 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Steve Tate ` (3 more replies) 2 siblings, 4 replies; 76+ messages in thread From: Robin Rowe @ 1995-04-20 0:00 UTC (permalink / raw) To: srt@zaphod.csci.unt.edu (Steve Tate) Sb: Re: What good is halting prob? Steve, << I would guess Robin has not actually had experience in proving correctness of programs from his comments, since they seem more like guesses as to what might be involved in the process (if I am wrong Robin, correct me!) >> Geez, Steve, I thought you liked me. Time for a refresher on that Dale Carnegie course? << Nope [to that proofs are based on what appears relevant to a human being to prove], proofs are based on formal specifications of the task at hand. >> So, it's not human beings who decide what belongs in the formal specifications? By the way, please define the term "formal" as you are using it here with regard to specifications. << This [that there is no proof that the proof is equivalent to the code] is based on a misconception, a proof of correctness, if is is any use at all, must have a formal relationship to the code. >> Please define the term "formal" as you are using it here. << Typically assertions in the code are used to guide an actual proof of the correctness of the actual code. Nothing else is useful. >> I'm not clear what you are trying to say here. Are you actually saying that the only really useful proofs are those expressed in code? (I think so, too, but this is a radical viewpoint!) << Proofs of correctness must be machine verified to be accepted. >> Please define the term "verified" as you are using it here. << Interfaces to components are part of the axiomatic structure of proven components, and on one side you prove that a component properly handles uses that conform to its interface, and on the other, you prove that the use by a client conforms to this interface. >> This sounds reasonable, and what I expected, too. However, I'm told that valid input parameter ranges are often specified arbitrarily. Invalid input is the user's (engineer's) lookout. Have I been misinformed? Is it generally more comprehensive? << I have no idea what you mean by random error. >> Cosmic rays, accidents, etc. << [Proofs take into account hardware failure] if the spec includes this, and they don't if the spec does not. >> Isn't this a pretty loose way to look at proof? Proving that you conformed to a (possibly erroneous) specification sounds a lot less impressive than saying you have a "proof of correctness." << I think you have an idea that a program that is proved correct is guaranteed to work. >> A mind reader you're not. << If you have a 100% track record in implementing code that exactly conforms to its specifications, wonderful! I think proof of correctness won't help, but if, like most people, you find that one of the many weak links on the chain is in incorrect implementation of specifications, then proof of correctness....>> Hmmm, I may have to change my mind about the utility of the halting problem. Implementing code that exactly conforms to its specifications sounds like the halting problem to me. Thanks for the feedback. Good points. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-20 0:00 ` Robin Rowe @ 1995-04-20 0:00 ` Steve Tate 1995-04-20 0:00 ` Apology to Steve Robin Rowe 1995-04-20 0:00 ` Problems with proofs Robert Dewar ` (2 subsequent siblings) 3 siblings, 1 reply; 76+ messages in thread From: Steve Tate @ 1995-04-20 0:00 UTC (permalink / raw) Robin Rowe (cpp@netcom.com) wrote: > To: srt@zaphod.csci.unt.edu (Steve Tate) > Sb: Re: What good is halting prob? > Steve, > << I would guess Robin has not actually had experience in proving > correctness of programs from his comments, since they seem more like > guesses as to what might be involved in the process (if I am wrong > Robin, correct me!) >> > Geez, Steve, I thought you liked me. Time for a refresher on that > Dale Carnegie course? > And much more deleted.... Whoa!!!!! I never said *any* of that! I have not made a single comment on proving correctness of programs --- I don't know much about that --- I have only made comments on computability and the halting problem. Was the posting you're citing really done under my name? I haven't seen it at all (and *certainly* didn't write it). It's either (1) a forgery or (2) you've gotten an attribute mixed up. -- Steve Tate --- srt@cs.unt.edu | "As often as a study is cultivated by narrow Dept. of Computer Sciences | minds, they will draw from it narrow University of North Texas | conclusions." -- John Stuart Mill, 1865. Denton, TX 76201 | ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Apology to Steve 1995-04-20 0:00 ` Steve Tate @ 1995-04-20 0:00 ` Robin Rowe 0 siblings, 0 replies; 76+ messages in thread From: Robin Rowe @ 1995-04-20 0:00 UTC (permalink / raw) In article <3n5t0c$nf4@hermes.unt.edu>, Steve Tate <srt@zaphod.csci.unt.edu> wrote: >Whoa!!!!! I never said *any* of that! Sorry Steve! Somehow I got your name tagged onto a post from Robert Dewar. Many apologies. I'm very sorry. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Steve Tate @ 1995-04-20 0:00 ` Robert Dewar 1995-04-21 0:00 ` Robin Rowe 1995-04-20 0:00 ` Robert Dewar 1995-04-21 0:00 ` Larry Kahn 3 siblings, 1 reply; 76+ messages in thread From: Robert Dewar @ 1995-04-20 0:00 UTC (permalink / raw) ><< I would guess Robin has not actually had experience in proving >correctness of programs from his comments, since they seem more like >guesses as to what might be involved in the process (if I am wrong > Robin, correct me!) >> You ascribed this to Steve, you are mixed up! It was me (Robert) who asked this, but in fact this note makes the answer pretty clear. I am beginning to understand your style. You make pronouncements on things you don't know much about in an attempt to provoke people into explaining them to you! OK I'm happy to play that game, once I understand it :-) :-) Anyway, please be assured this has nothing to do with liking you or not liking you. I don't even know you (for all I know you are a Turing test teletype doing a truly brilliant job :-) ><< Nope [to that proofs are based on what appears relevant to a >human being to prove], proofs are based on formal specifications of >the task at hand. >> >So, it's not human beings who decide what belongs in the formal >specifications? Sure, at some level this is true, but once the specification is constructed, it is no longer subject to human interpretation, and this is exactly what we mean by a formal spec, one whose semantics are mathematically specified, by some appropriate formalism, e.g. a reasonably powerful example would be first order predicate theory plus set theory. ><< This [that there is no proof that the proof is equivalent to the >code] is based on a misconception, a proof of correctness, if is is >any use at all, must have a formal relationship to the code. >> > >Please define the term "formal" as you are using it here. Again formal means that we have a formal specification as described above of both the language in which we write, and of the problem, and the formal relationship between the two is a proof that the program conforms to the specification. ><< Proofs of correctness must be machine verified to be accepted. >> >Please define the term "verified" as you are using it here. Proof verifiers are a very old technology, some early examples exist from the early 60's and maybe even late 50's. A proof verifier is simply a program (which had better be verified itself), that checks a proof to make sure that you have not goofed, i.e. it simulates a VERY accurate high school math teacher looking at your proofs on an exam. The technology of these verifiers has been studied for years, and there are many products both academic and commercial. ><< Interfaces to components are part of the axiomatic structure of >proven components, and on one side you prove that a component >properly handles uses that conform to its interface, and on the >other, you prove that the use by a client conforms to this >interface. >> > >This sounds reasonable, and what I expected, too. However, I'm told that >valid input parameter ranges are often specified arbitrarily. Invalid >input is the user's (engineer's) lookout. Have I been misinformed? Is it >generally more comprehensive? Sometimes yes, sometimes no, obviously if you are interfacing to the external world, you may simply have to start with a set of hopefully correct axioms about the behavior of the external world (here is a good place to build in your empirical safety factors if your information is imperfect). ><< I have no idea what you mean by random error. >> >Cosmic rays, accidents, etc. From a formal point of view, these are simply hardware errors. Mathematics does not care whether things have gone wrong because of acts of God, or because of manufacturing defects, leave that up to lawyers! ><< I think you have an idea that a program that is proved correct >is guaranteed to work. >> >A mind reader you're not. And still many of your comments seen disappointed that proof of correctness turns out only to be proof of conformance to (possibly incorrect) specifications. >Hmmm, I may have to change my mind about the utility of the halting >problem. Implementing code that exactly conforms to its >specifications sounds like the halting problem to me. I hope it is clear from my previous note that while it is trivially true that the conformance problem is equivalent to the halting problem, this is irrelevant. There is nothing that says that you can't prove that a given Turing machine halts, just that you can't do this in general. Similarly, we can't prove correctness in general, but we can do it in specific cases, which is what we are interested in. Robert (not Steve) (some of your quotes were indeed not from me, I did not answer them!) ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-20 0:00 ` Problems with proofs Robert Dewar @ 1995-04-21 0:00 ` Robin Rowe 1995-04-21 0:00 ` Robert Dewar 0 siblings, 1 reply; 76+ messages in thread From: Robin Rowe @ 1995-04-21 0:00 UTC (permalink / raw) In article <dewar.798390176@gnat>, Robert Dewar <dewar@cs.nyu.edu> wrote: >You ascribed this to Steve, you are mixed up! It was me (Robert) who asked >this, but in fact this note makes the answer pretty clear. I am beginning >to understand your style. You make pronouncements on things you don't know >much about in an attempt to provoke people into explaining them to you! OK >I'm happy to play that game, once I understand it :-) :-) Robert, I'm quite embarrassed to have attributed your rude remarks to Steve. What you really know about computer science is hard to judge, but you could learn a lot about social skills. Even if you were twice as brilliant as you think you are, it wouldn't give you the right to be obnoxious. It was my mistake in sinking to your level. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-21 0:00 ` Robin Rowe @ 1995-04-21 0:00 ` Robert Dewar 0 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-21 0:00 UTC (permalink / raw) Sorry, Robin, I certainly did not mean to be obnoxious (as you see in the reply to the note you misquoted, I tried to answer your questions in detail). I really did misinterpret your original comments on proof of correctness as rather surprising criticisms from someone aware of the technology, and it took a while to realize that you were not so familiar with the POC technology, and were really in the mode of trying to find out about it, which is why I tried to enlighten ... ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Steve Tate 1995-04-20 0:00 ` Problems with proofs Robert Dewar @ 1995-04-20 0:00 ` Robert Dewar 1995-04-21 0:00 ` Larry Kahn 3 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-20 0:00 UTC (permalink / raw) A more pragmatic note on proof of correctness and a real life example where it could be used. Yesterday, we got a most amazing GNAT bug report type signed_31 is range -2**30 .. +2**30-1; for signed'size use 31; didn't work, GNAT wanted 32 bits, yet this was one entry in a huge table with all possible sizes, and all the others worked fine. Investigation showed a definite bug in the universal integer add routine, it gave wrong results for very specific input. Now here is a really good example of where POC would be useful. The spec of the universal integer package is particularly well defined and simple at a mathematical level, since integers are really easy to talk about formally, even if their implementation is tricky! So, we can easily write the spec. Now, could we actually do the proof. Well first of all, we have to confine ourselves to a very simple subset, but I think we pretty much meet this, for example, I think this particular unit (Uintp in file uintp.ads/adb) is pretty much in the Praxis SPARK subset, for which a formal definition exists. You would have to hide one external interface, namely the access to the dynamically expanded tables (we don't want to get into storage allocation issues I think!) It would still be a VERY difficult business to prove. In particular, the proof of Knuth's Algorithm D for multi-precision division is definitely very hard. I would guess that this is right at the edge of the state of the art (I will ask a friend at Praxis what he thinks). But, if we had put the effort in, a POC of uintp would certainly have found this error, or rather made it impossible to prove that the code was correct. Of course you have to ask, is it worth it? And that's a tough one, proof of correctness techniqes at any level can get VERY expensive, which is why they are usually associated with high assurance code, where bugs are very costly, such as safety critical code. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-20 0:00 ` Robin Rowe ` (2 preceding siblings ...) 1995-04-20 0:00 ` Robert Dewar @ 1995-04-21 0:00 ` Larry Kahn 3 siblings, 0 replies; 76+ messages in thread From: Larry Kahn @ 1995-04-21 0:00 UTC (permalink / raw) In article <cppD7BMEw.2ts@netcom.com>, cpp@netcom.com says... > ><< [Proofs take into account hardware failure] if the spec includes >this, and they don't if the spec does not. >> > >Isn't this a pretty loose way to look at proof? Proving that you >conformed to a (possibly erroneous) specification sounds a lot less >impressive than saying you have a "proof of correctness." > ><< I think you have an idea that a program that is proved correct >is guaranteed to work. >> > hate to jump into this but I agree a proof of correctness is a formal method of proving that the program does what you expect it to do (WITH RESPECT TO A CERTAIN SPECIFICATION)!!!! this is the key... it is only correct with respect to the spec. and if your spec is in error of course the program will not perform correctly. The bottom line is that correctness is a relative term .. I may thing a program should print out a certain error message when certain conditions occur and this was not in the original spec and therefore the developers did not implement it. In terms of the developers the program may still be correct and even verifiable proved as correct with response to a certain spec ... but in my eyes I may say it is incorrect.. this the relativity of correctness (ie relative to individial opinion) But proof of correctness is a formal methodology for proving the program corresponds to what you expect it to do in relation to a specification and this is a different issue than whether or not I believe the program is correct in my eyes... You need to get a book on proof of correctness and look at the definitions more carefully proof of correctness does not proof that the program handles all possible values, never crashes, halts, etc..... I think this is what you are confusing with the term "correctness"..... -- Laurence G. Kahn Senior Software Engineer Dynamics Research Corp. (Finger .site@ambra.drcoffsite.com for PGP public key.) (Internet Phone address: LGK in private forum drcoffsite) ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <3n1fsv$lgd@butch.lmsc.lockheed.com>]
* Re: Problems with proofs [not found] ` <3n1fsv$lgd@butch.lmsc.lockheed.com> @ 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Garlington KE 0 siblings, 1 reply; 76+ messages in thread From: Robin Rowe @ 1995-04-20 0:00 UTC (permalink / raw) To: l107353@cliffy.lfwc.lockheed.com (Garlington KE) Sb: Re: Problems with proofs Ken, << Some of them [proofs] do [take into account combinatorial possibilities] - for example, Dr. Levison's state tables for the A-10 flight controls did, as I recall. >> Very interesting, where can I find out more? Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Problems with proofs 1995-04-20 0:00 ` Robin Rowe @ 1995-04-20 0:00 ` Garlington KE 0 siblings, 0 replies; 76+ messages in thread From: Garlington KE @ 1995-04-20 0:00 UTC (permalink / raw) Robin Rowe (cpp@netcom.com) wrote: : To: l107353@cliffy.lfwc.lockheed.com (Garlington KE) : Sb: Re: Problems with proofs : Ken, : << Some of them [proofs] do [take into account combinatorial : possibilities] - for example, Dr. Levison's state tables for the : A-10 flight controls did, as I recall. >> : Very interesting, where can I find out more? It seems like I remember a paper in the IEEE transactions on software engineering, but I'm not sure. I think I have Dr. Levison's E-mail address at home, or you can get it from one of the issues of RIsks Digest that came out recently. : Robin : -- : ----- : Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA : Rowe Technology C++ Design/Training Email for sample C++ Newsletter! -- -------------------------------------------------------------------- Ken Garlington GarlingtonKE@lfwc.lockheed.com F-22 Computer Resources Lockheed Fort Worth Co. If LFWC or the F-22 program has any opinions, they aren't telling me. ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <3me1qs$n4a@theopolis.orl.mmc.com>]
[parent not found: <3mevmu$8an@felix.seas.gwu.edu>]
[parent not found: <3mh75i$8eu@rational.rational.com>]
[parent not found: <3mjihr$iqq@felix.seas.gwu.edu>]
[parent not found: <3mp20f$80t@kaiwan009.kaiwan.com>]
* Re: Academic CS Losers? [not found] ` <3mp20f$80t@kaiwan009.kaiwan.com> @ 1995-04-20 0:00 ` Phillip Fanous 1995-04-21 0:00 ` Bill Winn 0 siblings, 1 reply; 76+ messages in thread From: Phillip Fanous @ 1995-04-20 0:00 UTC (permalink / raw) : (Since everyone laughs at making new languages or user interfaces : based on parsing, why should Compilers be a required course? For me, it was one of the more enlightening courses in my CS program. The book was pathetic, but the instructor was quite effective. Also, the main portion of the grade was based upon the implementation of a "baby C" compiler. For one thing, I gained a much deeper understanding of the C language (understanding the recursive nature of compiler functionality actually made looking at what I once thought was an obscure program not so obscure.) : 181 Formal languages and Automata Theory (Kill) I agree. That class is completely useless. : physics. We don't need to do combinatorial logic maps etc. We do not : really need to understand the details of hardware or worry about : "micro-coding" which is obsolete. Assembly coverage also should be : light. Instead we need to look at an architecture from a higher : level. "Arch I" should cover something like Tanenbaum Structured : Computer Org and "Arch II" should cover Patterson and Hennessy (now : used at graduate level). We sure don't need software people : doing "Radio Shack" projects in a lab. Networks is probably too : specific a topic to force at the undergrad level). I know this is probably geared more toward comp eng but what about embedded systems programming? It can't be that bad giving SW people an intro into the field of microprocessor HW/SW design. Granted, This field also requires a detailed understanding of electric circuits. : My opinion that lower division programming language should be done in : a done in a strongly typed imperitive object oriented language which : is very disiplined. Examples: Ada9x, Modula3, Oberon2. More : crackpot functional (Scheme/Lisp) and declaritive languages (Prolog) : would be covered in later programming languages classes. I am not : impressed with my department's current choices in programming : languages. I agree. This would make learning C++ much easier and would help the novice programmer in adopting the object-oriented design paradigm early so that they can develop good design habits. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: Academic CS Losers? 1995-04-20 0:00 ` Academic CS Losers? Phillip Fanous @ 1995-04-21 0:00 ` Bill Winn 0 siblings, 0 replies; 76+ messages in thread From: Bill Winn @ 1995-04-21 0:00 UTC (permalink / raw) In article <3n5410$pv1@crl.crl.com>, pfanous@crl.com writes... >: My opinion that lower division programming language should be done in >: a done in a strongly typed imperitive object oriented language which >: is very disiplined. Examples: Ada9x, Modula3, Oberon2. More >I agree. This would make learning C++ much easier and would help the >novice programmer in adopting the object-oriented design paradigm early >so that they can develop good design habits. > If the teaching of the Object paradigm is important, I believe teaching Smalltalk does better job than any of the aforementioned languages. Smalltalk does not allow one to fall out of the Object paradigm; hybrid languages allow one to use the Structured or (in some cases) the Hacking paradigms. I do, however, advocate the teaching of a strongly-typed language (e.g. Ada95) to students before unleashing C++ upon them. Bill Winn Software Engineer - Analysts International Corporation ------------------------------- wjwinn@kocrsv01.delcoelect.com wwinn@klingon.iupucs.iupui.edu My views do not express the views of anyone except my alter-ego. ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <3mrv7h$3mq@larry.rice.edu>]
[parent not found: <3msnu4$6am@kaiwan009.kaiwan.com>]
[parent not found: <KUBEK.95Apr18213646@insage.gerii.insa-tlse.fr>]
[parent not found: <cppD792GC.1uI@netcom.com>]
* Re: Teaching OO/C++ [not found] ` <cppD792GC.1uI@netcom.com> @ 1995-04-20 0:00 ` Philip Machanick 0 siblings, 0 replies; 76+ messages in thread From: Philip Machanick @ 1995-04-20 0:00 UTC (permalink / raw) In article <cppD792GC.1uI@netcom.com>, cpp@netcom.com (Robin Rowe) wrote: > This is what tends to happen if you teach C first. How do you decide > when to call it quits and tell the students to forget half of everything > they learned to switch to C++? You don't have this difficulty if you > teach OO first, then present the syntax as support of it. (You have other > problems, like finding a textbook written this way.) I fully agree. I started my 2nd year class off (previously exposed to Pascal) with abstraction, classes and objects -- in that order. I spent less than 10% of my lectures on syntax. They whined terribly about C++ syntax at first, but I just let them pick it up as we went along. It's been quite a while now since I saw someone trying to get FOR i:= 1 TO n DO past the compiler :( If you don't think OOP is better than a procedural style of programming, why teach it at all? This reminds me about the bad old days when Pascal text books did procedures last and recursion as an appendix (not quite that bad I suppose). I used to argue in those days that if this is the order you do things, you might as well teach FORTRAN. -- Philip Machanick philip@cs.wits.ac.za Department of Computer Science, University of the Witwatersrand 2050 Wits, South Africa phone 27(11)716-3309 fax 27(11)339-7965 ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <cppD75t6F.47M@netcom.com>]
[parent not found: <EACHUS.95Apr17172831@spectre.mitre.org>]
[parent not found: <cppD77Ex6.E77@netcom.com>]
[parent not found: <3mve9b$gaj@news.cais.com>]
* Re: What good is halting prob? [not found] ` <3mve9b$gaj@news.cais.com> @ 1995-04-18 0:00 ` Jay M Martin 1995-04-19 0:00 ` Steve Tate [not found] ` <cppD7880n.32B@netcom.com> 1 sibling, 1 reply; 76+ messages in thread From: Jay M Martin @ 1995-04-18 0:00 UTC (permalink / raw) In <3mve9b$gaj@news.cais.com> crawford@cais2.cais.com (Randolph Crawford) writes: >As a final point, one of the reasons why this stuff is often presented >as part of a CS theory course on formal automata is the simplicity of >showing undecidability and the halting problem using Turing machines. >Once the student understands that this undecidability holds for Turing >machines, it becomes clear that it holds for all kinds of languages/ >automata/machines as well, like BASIC and C. >It also happens that this class of undecidable programs is called >Universal Turing Machines -- which is another reason to introduce the >halting problem and undecidability at the same time as Turing machines. I think Turing machines are pretty silly and see an idealized register or random access machine as a much better way to present this stuff. To me its just one of many "Dumb ideas of Computer Science" that are sort of anarchisms but still survive. I put lambda calculus and algol style nesting in this category too. Jay ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-18 0:00 ` What good is halting prob? Jay M Martin @ 1995-04-19 0:00 ` Steve Tate 1995-04-20 0:00 ` Jay M Martin 1995-04-21 0:00 ` Ray Toal 0 siblings, 2 replies; 76+ messages in thread From: Steve Tate @ 1995-04-19 0:00 UTC (permalink / raw) Jay M Martin (jmartin@kaiwan009.kaiwan.com) wrote: > I think Turing machines are pretty silly and see an idealized register > or random access machine as a much better way to present this stuff. Gee, it's nice of you to back this up with such solid reasoning! "Turing machines are pretty silly" --- what a great argument! Sarcasm off. I have seen concepts from the theory of computing (both computability and complexity) presented in many different ways, including a presentation using register machines made by a famous mathematician/logician/recursion theorist. Let me tell you this --- dealing with machine and state descriptions is much more elegant using a Turing machine than in *any* other model that I've seen. The proof of Cook's theorem (NP-completeness) is fairly clean for a Turing machine, but becomes messy if you try to use a RAM. The other point to make is that you should think about the Church-Turing thesis. If approached from the point of view of a RAM, it's easy to have many doubts, such as how does the instruction set affect the computing power of the machine? On the other hand, when looked at from the point of view of Turing machines, it seems like almost an obvious statement. Finally, for computational complexity issues such as how big registers are and what the instruction set is *do* strongly affect the results. There are no such "unseen assumptions" with Turing machines. > To me its just one of many "Dumb ideas of Computer Science" that are > sort of anarchisms but still survive. Do you *really* think it has stuck around this long as the primary model of computation for theory of computing work from momentum rather than usefulness? If other models are better, why are new proofs written using Turing machines? Let me tell you why: because the proofs are clean and elegant. I've heard complaints about Turing machines before, but almost entirely from people who don't appreciate the theoretical work that uses them. -- Steve Tate --- srt@cs.unt.edu | "As often as a study is cultivated by narrow Dept. of Computer Sciences | minds, they will draw from it narrow University of North Texas | conclusions." -- John Stuart Mill, 1865. Denton, TX 76201 | ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Steve Tate @ 1995-04-20 0:00 ` Jay M Martin 1995-04-21 0:00 ` Steve Tate 1995-04-21 0:00 ` Ray Toal 1 sibling, 1 reply; 76+ messages in thread From: Jay M Martin @ 1995-04-20 0:00 UTC (permalink / raw) In <3n3b82$ild@hermes.unt.edu> srt@zaphod.csci.unt.edu (Steve Tate) writes: >Jay M Martin (jmartin@kaiwan009.kaiwan.com) wrote: >> I think Turing machines are pretty silly and see an idealized register >> or random access machine as a much better way to present this stuff. >Gee, it's nice of you to back this up with such solid reasoning! >"Turing machines are pretty silly" --- what a great argument! I think "silly" is a good discription for Turing machines, Goofy is another. Come on, they are silly Rube Goldberg machines stamping symbols on infinite tapes that can move back and forth one position at a time. Not my idea of a modern high-performance computer architecture! >I have seen concepts from the theory of computing (both computability >and complexity) presented in many different ways, including a >presentation using register machines made by a famous >mathematician/logician/recursion theorist. Let me tell you this --- >dealing with machine and state descriptions is much more elegant using >a Turing machine than in *any* other model that I've seen. The proof >of Cook's theorem (NP-completeness) is fairly clean for a Turing >machine, but becomes messy if you try to use a RAM. For the halting problem, I found the register machine approach clearer. As for Cook's theorem look at Cormen for practical and elegant proof. No turing machines, no wierd definitions of NP-complete as what is computable by a "non-deterministic Turing machine" in polynomial time. The proof is simpler than any Turing machine proof I have ever seen. Plus register machines, circuits etc, build on useful computer concepts, not on some minimalist and useless (in a practical sense) machine. >The other point to make is that you should think about the >Church-Turing thesis. If approached from the point of view of a RAM, >it's easy to have many doubts, such as how does the instruction set >affect the computing power of the machine? On the other hand, >when looked at from the point of view of Turing machines, it seems >like almost an obvious statement. >Finally, for computational complexity issues such as how big registers >are and what the instruction set is *do* strongly affect the results. >There are no such "unseen assumptions" with Turing machines. But this is assuming that this (possibly extra) thinking about these issues with register/random access machines is not useful. But it is useful because these models are close to real machines and thus are important to computer understanding in general. As I see it, understanding apparent paradoxes (doubts) with these machine models is worth the (possibly) extra effort. >> To me its just one of many "Dumb ideas of Computer Science" that are >> sort of anarchisms but still survive. >Do you *really* think it has stuck around this long as the primary >model of computation for theory of computing work from momentum >rather than usefulness? If other models are better, why are new >proofs written using Turing machines? Let me tell you why: because >the proofs are clean and elegant. Yes, I do. Computer Science (and other human endeavors) is filled with silly, failed, culdesac-ed and incestuous fields and notations. Are the proofs clean and elegant, or are you such a savant at Turing Machines that they are "elegant" to you. Maybe the proofs would be more accessable to others if you guys stopped using Turing Machines. So basically, as I see it, both the halting problem and NP-Completeness can be presented without turing machines. Since these approaches more directly model real computers thus building on and teaching practical computer concepts (circuits,random access machines), I would expect students to connect more fully with this approach (because it closer to reality). So basically, I see no pressing need to teach Turing Machines to 2 and 3rd year undergraduate CS majors, it can taught to those specializing in the complexity field. Now get back to proving P != NP, I am tired of waiting. :-) Jay ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-20 0:00 ` Jay M Martin @ 1995-04-21 0:00 ` Steve Tate 0 siblings, 0 replies; 76+ messages in thread From: Steve Tate @ 1995-04-21 0:00 UTC (permalink / raw) Jay M Martin (jmartin@kaiwan009.kaiwan.com) wrote: > In <3n3b82$ild@hermes.unt.edu> srt@zaphod.csci.unt.edu (Steve Tate) writes: > >I have seen concepts from the theory of computing (both computability > >and complexity) presented in many different ways, including a > >presentation using register machines made by a famous > >mathematician/logician/recursion theorist. Let me tell you this --- > >dealing with machine and state descriptions is much more elegant using > >a Turing machine than in *any* other model that I've seen. The proof > >of Cook's theorem (NP-completeness) is fairly clean for a Turing > >machine, but becomes messy if you try to use a RAM. > For the halting problem, I found the register machine approach > clearer. As for Cook's theorem look at Cormen for practical and > elegant proof. No turing machines, no wierd definitions of > NP-complete as what is computable by a "non-deterministic Turing > machine" in polynomial time. The proof is simpler than any Turing > machine proof I have ever seen. In a partial way, what you say is true, but if you look a little more carefully at the presentation in CLR it actually supports what I said above. The concepts of NP-completeness are presented in a very clean and clear way in CLR. But not using Turing machines makes the proof of Cook's theorem messy and difficult. In fact, it gets so messy that CLR doesn't even present the full proof!!! To quote them: "The actual proof of this fact is full of technical intricacies, and so we shall settle for a sketch of the proof based on some understanding of the workings of computer hardware." Using a Turing Machine the proof is very clear and isn't based on some vague "understanding of the workings of computer hardware". > Plus register machines, circuits etc, > build on useful computer concepts, not on some minimalist and useless > (in a practical sense) machine. It depends on what you call "practical". If you're interested in writing programs, then Turing machines aren't very practical. If you're interested in proving theorems, they *are* very practical. > >The other point to make is that you should think about the > >Church-Turing thesis. If approached from the point of view of a RAM, > >it's easy to have many doubts, such as how does the instruction set > >affect the computing power of the machine? On the other hand, > >when looked at from the point of view of Turing machines, it seems > >like almost an obvious statement. > >Finally, for computational complexity issues such as how big registers > >are and what the instruction set is *do* strongly affect the results. > >There are no such "unseen assumptions" with Turing machines. > But this is assuming that this (possibly extra) thinking about these > issues with register/random access machines is not useful. But it is > useful because these models are close to real machines and thus are > important to computer understanding in general. As I see it, understanding > apparent paradoxes (doubts) with these machine models is worth the > (possibly) extra effort. Very true --- but doesn't it make sense to lay down the unambiguous framework (using Turing Machines) first, and then use that as a basis for discussing the apparent paradoxes with the more computer-hardware oriented models? If you don't establish the firm basis first, what do you use as a point of reference? > >> To me its just one of many "Dumb ideas of Computer Science" that are > >> sort of anarchisms but still survive. > >Do you *really* think it has stuck around this long as the primary > >model of computation for theory of computing work from momentum > >rather than usefulness? If other models are better, why are new > >proofs written using Turing machines? Let me tell you why: because > >the proofs are clean and elegant. > Yes, I do. Computer Science (and other human endeavors) is filled > with silly, failed, culdesac-ed and incestuous fields and notations. > Are the proofs clean and elegant, or are you such a savant at Turing > Machines that they are "elegant" to you. Maybe the proofs would be > more accessable to others if you guys stopped using Turing Machines. Are you claiming that proofs need to be accessible to someone not trained in the field? I don't understand why that's a particularly good goal at all. Imagine if someone had said to Wiles "My, that's a nice proof of Fermat's Last Theorem, but why didn't you write it in a way that's accessible to everyone?" The point is, that work builds on other work --- if there is an easier and more elegant way to approach the work it will be taken, but to make proofs more complicated in order to base them on more common ground is not a direction I'm interested in taking. > So basically, as I see it, both the halting problem and > NP-Completeness can be presented without turing machines. Since these > approaches more directly model real computers thus building on and > teaching practical computer concepts (circuits,random access > machines), I would expect students to connect more fully with this > approach (because it closer to reality). So basically, I see no > pressing need to teach Turing Machines to 2 and 3rd year undergraduate > CS majors, it can taught to those specializing in the complexity > field. And I see no pressing need to "dumb down" the curriculum by not talking about Turing machines. It may take a different outlook than the typical "program this" attitude of many other courses, but struggling to get the concepts is very valuable and provides excellent additional insight. Education isn't supposed to always be easy or entertaining, and we are trying to educate computer *scientists*, not computer *programmers*. -- Steve Tate --- srt@cs.unt.edu | "As often as a study is cultivated by narrow Dept. of Computer Sciences | minds, they will draw from it narrow University of North Texas | conclusions." -- John Stuart Mill, 1865. Denton, TX 76201 | ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Steve Tate 1995-04-20 0:00 ` Jay M Martin @ 1995-04-21 0:00 ` Ray Toal 1 sibling, 0 replies; 76+ messages in thread From: Ray Toal @ 1995-04-21 0:00 UTC (permalink / raw) In article <3n3b82$ild@hermes.unt.edu> srt@zaphod.csci.unt.edu (Steve Tate) writes: >I have seen concepts from the theory of computing (both computability >and complexity) presented in many different ways, including a >presentation using register machines made by a famous >mathematician/logician/recursion theorist. Here's one that just uses Ada 95 (sorry if this is common knowledge): Given: type Program is access procedure; We want to write: function Halts (P: Program) return Boolean; But we cannot because we can write procedure Nasty is begin if Halts (Nasty'Access) then loop null; end loop; end if; end Nasty; which halts if and only if it doesn't. I've found this an effective way to present the halting problem to students who have not yet seen Turing Machines. (Of course, before Ada 95, I had to show them in C++ due to the lack of subprograms as parameters in Ada 83.) Ray Toal ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <cppD7880n.32B@netcom.com>]
* Re: What good is halting prob? [not found] ` <cppD7880n.32B@netcom.com> @ 1995-04-19 0:00 ` Randolph Crawford 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 1995-04-21 0:00 ` sxc 1 sibling, 2 replies; 76+ messages in thread From: Randolph Crawford @ 1995-04-19 0:00 UTC (permalink / raw) In article <cppD7880n.32B@netcom.com>, Robin Rowe <cpp@netcom.com> wrote: >In article <3mve9b$gaj@news.cais.com>, >Randolph Crawford <crawford@cais2.cais.com> wrote: >>If you can identify a different problem as being basically the same as >>the halting problem.... > >The "if" was the point of my question. How do you prove equivalence to >the halting problem? Short of formal substitution or equivalence proofs, you recognize the same potential for failure, the likelihood that your program will not terminate as expected due to the introduction of data whose influence you cannot anticipate. > >>Let's say you wrote a program that you wanted to be "correct". >>[...] It behaves as it should, it halts, it's deterministic >>and decidable. You might conclude from having writen such a program that >>with enough effort on the part of the programmer, *every* program could be >>written the way this one was, ensuring correctness. But you'd be mistaken. > >Well, if anyone can write one non-trivial program to be "correct" I would >then be willing to reconsider if the general case is attainable. Until >then, I'm not in much danger of falling into the trap you suggest. If >someday machines become more intelligent than we are, correctness may >become very difficult to judge. Correctness itself is a very subjective term. You want a trivial correct program? main() { if (1) exit( 0); } It ain't much, but it's correct. It's easy to write correct programs. It's just that some programs (the UTMs or those programs that contain UTMs) can never be proven correct. And correctness is not subjective. It simply means that the program will always behave as expected, regardless of the input. If by correctness, you are thinking of "not incorrect", or "acceptably correct", there's a difference. You're talking about points on a continuum. Correct is clear at one end; it's perfect. You can write a program that performs properly in most or nearly all cases but fails to terminate under only ONE pathological input value, and while that program may be acceptable, it's not correct. It's equally possible for a correct program to do nothing useful. My point is, it's correct as long as it behaves entirely predictably (decidably). (Correctness doesn't have to be a reasonable demand on a program. It's an immutable point of reference, like "truth" or "justice".) > [...] >Perhaps I'm taking you too literally here. You can, of course, defend >yourself from anything you anticipate, but deciding what to if an event >occurs may not be feasible. Taking your example of divide by zero, this >halts any machine that I am familiar with. Do you feel any concern that it >won't halt? Yes, the program halts. The choice of halting (by the great masters of CS) was a somewhat arbitrary one. It's just a measure of whether a program is correct. (As it happens, properly functioning turing machines are supposed to do several things when they execute, one of which is halt. Ergo the choice of "not halting" as a measure of incorrectness.) Division by zero isn't important except as an exmple of failure. Likewise the inability to halt is a good example of failure. You can be certain of anticipating both of these failures *only* if your program is not a Universal Turing Machine. If it is a UTM, you cannot be certain that it will behave as you planned, because you cannot constrain your input data sufficiently. That's the purpose behind teaching the halting proglem. Yes, you can constrain the input of many programs to make them correct. You can constrain many more programs to make them *sufficiently* correct. But some programs can never be considered correct in light of the way they respond to data (by treating them as programs themselves). While this last class of programs may be relatively small, it illustrates the existence of a potential threat to any program. Like exponential search and NP-hardness, it's good to know the limits to how certain of perfection (and safety) you really can be when writing software. > >[...] No one expects every potential bridge or building design to be >decidedly correct. Designs are purposely engineered to be easy to analyze >(model). Is this remarkable? I think the blurring of the difference between software and bridges is where the confusion lies. No bridge can be proven correct. But it's traditional that the mathematical foundations used in building bridges *are* considered correct, ie. perfect. If a civil engineer found that error was cropping up in his computations *without his/her knowing* then any bridge or building he builds is at greater risk than he intended. THAT's the point behind correctness and the halting problem in computer science-- knowing that you can't assume *too much* when you write code. -- Randy crawford@mrj.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Randolph Crawford @ 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 1 sibling, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-19 0:00 UTC (permalink / raw) Randy says: "And correctness is not subjective. It simply means that the program will always behave as expected, regardless of the input. If by correctness, you are thinking of "not incorrect", or "acceptably correct ..." I think that's potentially misleading. Correctness has to do with conformance to a formal specification, at least the way the term is used when you talk about "proof of correctness". Suppose you expect a compiler to always give clear understandable error messages. That's a reasonable expectation, but you can't formalize it. So correctness could not capture this informal expectation. On the other hand, given a formal definition of the language you are compiling, it is at least conceptually feasible to prove that a compiler gives an error message of *some* kind for any incorrect program. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Randolph Crawford 1995-04-19 0:00 ` Robert Dewar @ 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Robert Dewar 1 sibling, 1 reply; 76+ messages in thread From: Robin Rowe @ 1995-04-20 0:00 UTC (permalink / raw) To: crawford@cais2.cais.com (Randolph Crawford) Sb: Re: What good is halting prob? Randy, >You want a trivial correct program? > >main() >{ > if (1) exit( 0); >} > >It ain't much, but it's correct. Ok, here's the program's specification: "The program will report an error to the operating system on exit. An exit code of zero is not valid." Still think this code is correct? You might say this isn't fair, and I would agree. However, I think it illustrates my point that correctness is subjective. << If by correctness, you are thinking of "not incorrect", or "acceptably correct", there's a difference. >> I'm talking about proofs of correctness, where correctness is judged relative to a specification. << My point is, it's correct as long as it behaves entirely predictably (decidably). >> This is a very interesting definition. Most seem to feel that correctness is adherence to the specification. Given the combinatorial mathematics, correctness under your definition would seem to imply the halting problem. I guess I might as well give up my notion that the halting problem isn't useful. I've used it twice now in this thread. << Division by zero isn't important except as an exmple of failure. Likewise the inability to halt is a good example of failure. You can be certain of anticipating both of these failures *only* if your program is not a Universal Turing Machine. >> I can assure you that not one of my programs operates an infinite tape. ;-) << I think the blurring of the difference between software and bridges is where the confusion lies. No bridge can be proven correct. But it's traditional that the mathematical foundations used in building bridges *are* considered correct, ie. perfect. If a civil engineer found that error was cropping up in his computations *without his/her knowing* then any bridge or building he builds is at greater risk than he intended. >> If you mean that F=ma is the mathematical foundation then yes, that operates pretty well on bridges up to the speed of light. However, the state of the art is constantly improving in bridge modeling. After the LA quake, in which some bridges failed that shouldn't have, I recall a civil engineer quoted as saying they learn something new from every earthquake. The notorious Tacoma Narrows Galloping Gerty failure was due to a failure in the correctness of the mathematical model. Aerodynamic forces had not previously been considered. (Two earlier bridges failed for the same reason, but there wasn't any newsreel footage.) Engineers routinely build a safety factor into their designs in allowance for imperfections in the mathematical model. Except software engineers. Thanks for the feedback. Good points. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-20 0:00 ` Robin Rowe @ 1995-04-20 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 0 siblings, 1 reply; 76+ messages in thread From: Robert Dewar @ 1995-04-20 0:00 UTC (permalink / raw) Robin is certainly right to point out that a program on its own cannot usefully be said to be correct or incorrect, there must be an accompanying specification. Still I don't see that this means that correctness is subjective. Not at all, it is an objective function Correct (P : Program; S : Specification) return Boolean; of course the halting problem says that we cannot provide a full implementation of correct. But that brings up another point. Of course correctness is (pretty trivially) equivalent to the halting problem, and thus is undecidable. But Robin, don't make the mistake of assuming that because a problem is undecidable it is impossible to write a program that decides it in most or some cases. For any given instance of the halting problem, there is of course an answer. Either the program halts or it does not halt. Furthermore there is a trivial program, for a particular instance of the halting problem, that gives the right answer (it is one of the following: return True or return False of course it may be hard to tell which of these two giving the right answer! Suppose now we go back to our correctness function: program x spec => boolean obviously we can't write this program in a way that it always works, but we could write a program which would do one of three things: result in true result in false go into an infinite loop in fact it is not hard to write this program, we just enumerate proofs till we find one that proves correctness or incorrectness (at least I should say not hard conceptually, the mechanics of this program would of course be formidable). So that's an important lesson, just because something is equivalent tto the halting problem does not mean that we can't write a program for it, it just means that the program can't possibly work in all cases. So it would be a good idea to change the spec of our correctness procedure to return a type type result is (correct, incorrect, cannot_tell) instead of boolean. and expect it to generate a proof along with correct, a counter-example along with incorrect. then our task as a programmer is simply to avoid the cannot_tell cases in our programs if we are interested in correct programs. We may have to discard some perfectly good and correct programs, but a correct program that you cannot convince anyone else is correct is a dubious beast. ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-20 0:00 ` Robert Dewar @ 1995-04-20 0:00 ` Robin Rowe 1995-04-21 0:00 ` Brian Hanson 0 siblings, 1 reply; 76+ messages in thread From: Robin Rowe @ 1995-04-20 0:00 UTC (permalink / raw) In article <dewar.798381929@gnat>, Robert Dewar <dewar@cs.nyu.edu> wrote: >Robin is certainly right to point out that a program on its own cannot >usefully be said to be correct or incorrect.... I didn't go quite that far. I can envision the program itself being the specification. In fact, I see no other way to guarantee that a program really matches its specification. >But Robin, don't make the mistake of assuming that because a problem is >undecidable it is impossible to write a program that decides it in >most or some cases. Not only don't I make this mistake, it is the tendency toward that misconception on the part of halting problem believers that made me question its value in the first place. However, now that I've used the halting problem a couple time in replies on this thread I have new respect for the halting problem's usefulness. >then our task as a programmer is simply to avoid the cannot_tell cases >in our programs if we are interested in correct programs. In practice it is not feasible to statically eliminate the cannot_tell cases because a real computer doesn't have an infinite tape (or time). It can be painted into a corner. What I think is achievable is to design a program that knows it doesn't know and fails gracefully. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-20 0:00 ` Robin Rowe @ 1995-04-21 0:00 ` Brian Hanson 0 siblings, 0 replies; 76+ messages in thread From: Brian Hanson @ 1995-04-21 0:00 UTC (permalink / raw) In article 3v1@netcom.com, cpp@netcom.com (Robin Rowe) writes: > In practice it is not feasible to statically eliminate the cannot_tell > cases because a real computer doesn't have an infinite tape (or time). It > can be painted into a corner. What I think is achievable is to design a > program that knows it doesn't know and fails gracefully. BZZZZT! Wrong. You can design a program to fail gracefully but you cannot in general design a program to know that it doesn't know. You can have a program attempt a calculation and give it a time limit to accomplish it but your program cannot know whether the calculation would have finished one microsecond after your time limit or taken forever. -- -- Brian Hanson -- brh@cray.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? [not found] ` <cppD7880n.32B@netcom.com> 1995-04-19 0:00 ` Randolph Crawford @ 1995-04-21 0:00 ` sxc 1 sibling, 0 replies; 76+ messages in thread From: sxc @ 1995-04-21 0:00 UTC (permalink / raw) In article <cppD7880n.32B@netcom.com>, Robin Rowe <cpp@netcom.com> wrote: >In article <3mve9b$gaj@news.cais.com>, >Randolph Crawford <crawford@cais2.cais.com> wrote: >>If you can identify a different problem as being basically the same as >>the halting problem.... > >The "if" was the point of my question. How do you prove equivalence to >the halting problem? You don't need to >prove< equivalence of a problem to the halting problem for it to be of practical use. You only need to be able to >recognise< that your problem is essentially the same as, or subsumes the halting problem. The same goes for complexity (big-O) analysis in many cases. I often find it useful to do informal complexity estimates when designing or reviewing software. -- Steve ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <dewar.798172270@gnat>]
[parent not found: <cppD786FM.1u9@netcom.com>]
* Re: What good is halting prob? [not found] ` <cppD786FM.1u9@netcom.com> @ 1995-04-19 0:00 ` Mark A Biggar 1995-04-19 0:00 ` Richard Ladd Kirkham [not found] ` <dewar.798207364@gnat> 1 sibling, 1 reply; 76+ messages in thread From: Mark A Biggar @ 1995-04-19 0:00 UTC (permalink / raw) In article <cppD786FM.1u9@netcom.com> cpp@netcom.com (Robin Rowe) writes: >In article <dewar.798172270@gnat>, Robert Dewar <dewar@cs.nyu.edu> wrote: >>...problems isomorphic to the halting >>problem come up all the time. One quick example, the other day, someone >>asked why compilers refused to detect undefined variables, and some people >>seem to think that this is actually possible, while of course it is provably >>impossible (you can detect some simple casees, but not all cases >>statically). >I don't normally write compilers, so I haven't encountered this question. >This seems like it could be a very good example, thanks! One thing though, I >don't see how you can prove that this is equivalent to the halting >problem for any compiler that might be written. Can you show this in the >general case? If not, what language of compiler do you have a proof for, >and how did you construct it? It turns out that the compiler doesn't matter at all here, it's the language you are trying to compile that determines if uninitializized variable detection, dead code elimination, several kinds of erroneous execution, etc. in that language is equivalent to the Halting Problem. The language just has be sufficiently complex for this to be a necessary consideration. I believe that, for example, that any language with unbounded loops or unbounded recursion is sufficient. Another example: determining if changing the parameter passing method from by-refernece to copy-in-copy-out and vis-versa changes the behaviour of your program is also equivalent to the Halting Problem. The Ada83 LRM says that such programs are erroneous, but the above result means that detecting such programs at compile time is not possible in gerneral. Someone once said: "All interesting problems in CS are either trivial, NP-Complete or equivalent to the Halting Problem". I would like to track down this quote so I can attribute it correctly in the furture, can anyone help? -- Mark Biggar mab@wdl.loral.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Mark A Biggar @ 1995-04-19 0:00 ` Richard Ladd Kirkham 1995-04-19 0:00 ` Robert Dewar 1995-04-21 0:00 ` Mark A Biggar 0 siblings, 2 replies; 76+ messages in thread From: Richard Ladd Kirkham @ 1995-04-19 0:00 UTC (permalink / raw) In article <1995Apr19.204744.21914@wdl.loral.com> mab@dst17.wdl.loral.com (Mark A Biggar) writes: > >Another example: determining if changing the parameter passing method from >by-refernece to copy-in-copy-out and vis-versa changes the behaviour of >your program is also equivalent to the Halting Problem. The Ada83 LRM >says that such programs are erroneous, but the above result means that >detecting such programs at compile time is not possible in gerneral. > I don't get this. *What* programs is the LRM calling erroneous? Also, aside from a hardware failure or hardware inadequacy, wouldn't two other wise identical programs, one using by-reference and the other copy-in-copy back, behave identically? -- Richard Ladd Kirkham Georgia Institute of Technology, Atlanta Georgia, 30332 uucp: ...!{decvax,hplabs,ncar,purdue,rutgers}!gatech!prism!gt2782a Internet: gt2782a@prism.gatech.edu ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Richard Ladd Kirkham @ 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Richard Ladd Kirkham 1995-04-21 0:00 ` Mark A Biggar 1 sibling, 1 reply; 76+ messages in thread From: Robert Dewar @ 1995-04-19 0:00 UTC (permalink / raw) It is easy to construct examples where the effect depends on the parameter passing mechanism: procedure X (a, b : in out string) is begin a(1) := 'x'; if b(1) = 'x' then raise program_error; end if; end x; G : string := "abc"; H : string := "def"; X (G, H); will raise program error if the strings are passed by reference but not if they are passed by copy. In Ada 83 this program execution is erroneous but effect is not very well defined and so in Ada 95, a simpler definition is made that this program is simply non-deterministic (i.e. it may do one of two well defined things, depending on the parameter passing method). ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Robert Dewar @ 1995-04-20 0:00 ` Richard Ladd Kirkham 1995-04-20 0:00 ` Robert Dewar 0 siblings, 1 reply; 76+ messages in thread From: Richard Ladd Kirkham @ 1995-04-20 0:00 UTC (permalink / raw) In article <dewar.798337304@gnat> dewar@cs.nyu.edu (Robert Dewar) writes: >It is easy to construct examples where the effect depends on the parameter >passing mechanism: > > procedure X (a, b : in out string) is > begin > a(1) := 'x'; > if b(1) = 'x' then raise program_error; end if; > end x; > > G : string := "abc"; > H : string := "def"; > X (G, H); > >will raise program error if the strings are passed by reference but not >if they are passed by copy. In Ada 83 this program execution is erroneous Sorry. But I don't get it. When the branch condition is reached, b(1) = 'd' regardless of whether b is a reference or only a copy of H. -- Richard Ladd Kirkham Georgia Institute of Technology, Atlanta Georgia, 30332 uucp: ...!{decvax,hplabs,ncar,purdue,rutgers}!gatech!prism!gt2782a Internet: gt2782a@prism.gatech.edu ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-20 0:00 ` Richard Ladd Kirkham @ 1995-04-20 0:00 ` Robert Dewar 0 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-20 0:00 UTC (permalink / raw) sorry, no wonder you "don't get it", I messed up the example. here is the example I meant to give: procedure X (a, b : in out string) is begin a(1) := 'x'; if b(1) = 'x' then raise program_error; end if; end x; G : string := "abc"; X (G, G); will raise program error if the strings are passed by reference but not if they are passed by copy. In Ada 83 this program execution is erroneous and in Ada 95 it is non-deterministic (may or may not raise PE). Sorry about that! ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Richard Ladd Kirkham 1995-04-19 0:00 ` Robert Dewar @ 1995-04-21 0:00 ` Mark A Biggar 1 sibling, 0 replies; 76+ messages in thread From: Mark A Biggar @ 1995-04-21 0:00 UTC (permalink / raw) In article <3n429h$pvu@acmex.gatech.edu> gt2782a@prism.gatech.edu (Richard Ladd Kirkham) writes: >In article <1995Apr19.204744.21914@wdl.loral.com> mab@dst17.wdl.loral.com (Mark A Biggar) writes: >> >>Another example: determining if changing the parameter passing method from >>by-refernece to copy-in-copy-out and vis-versa changes the behaviour of >>your program is also equivalent to the Halting Problem. The Ada83 LRM >>says that such programs are erroneous, but the above result means that >>detecting such programs at compile time is not possible in gerneral. >I don't get this. *What* programs is the LRM calling erroneous? Also, >aside from a hardware failure or hardware inadequacy, wouldn't two other >wise identical programs, one using by-reference and the other copy-in-copy >back, behave identically? No they don't behave identically. The whole point is that it IS possible to write programs where the choice of parameter passing method results in different behaviour. This usually happens with multiply aliased parameters, for example: subtype name is string(1..3); var: name := "abc"; procedure test(a,b: in out name) is begin a(1) := 'd'; if b(1) = 'd' then raise constraint_error end if; end test; Now look at the call "test(var, var);": if the parameter passing method is by-reference then the call will raise constraint_error, but if copy-in-copy-back is used it won't raise the exception because the assignemnt to a(1) is made to a different copy then the test on b(1). The Ada83 LRM calls such code erroneous, while the Ada95 LRM makes it only a bounded error as there are only 2 possible results and both are well defined. But you can't require the complier to detect such code as doing so can be shown to be reducable to the halting problem. There is a paper is a early issue of Ada Letters about this. -- Mark Biggar mab@wdl.loral.com ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <dewar.798207364@gnat>]
[parent not found: <cppD78xMv.49w@netcom.com>]
* Re: What good is halting prob? [not found] ` <cppD78xMv.49w@netcom.com> @ 1995-04-19 0:00 ` Robb Nebbe 0 siblings, 0 replies; 76+ messages in thread From: Robb Nebbe @ 1995-04-19 0:00 UTC (permalink / raw) : : If b was declared as a class member, then you can tell if it is initialized : by the constructor. In OOP, global data is a no-no, so b would either be : a class member or a local variable. Where an order of initialization : dependency exists between two objects, there could be some trouble, but : static initializers can deal with this (as in the standard library : iostreams.h). If b is a local it is even easier to detect initialization. : With reasonable constraints on the language, detecting initialization seems : feasible to me. What am I missing? You always have the three cases: it is initialized, it isn't initialized or you can't tell. By carefully designing the language (or through careful use of the language) you can eliminate the case where you can't tell. But then you are not dealing with a general solution; you have restricted the problem space to a particular case of interest which is often sufficient. By the way default constructors really don't count as initialization. They have a legal value but often it isn't meaningful -- it is just some neutral value. Robb Nebbe ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <3n0ka7$b57@hermes.unt.edu>]
[parent not found: <dewar.798232482@gnat>]
* Re: What good is halting prob? [not found] ` <dewar.798232482@gnat> @ 1995-04-19 0:00 ` Mark A Biggar 1995-04-19 0:00 ` Robert Dewar 1995-04-19 0:00 ` Steve Tate 0 siblings, 2 replies; 76+ messages in thread From: Mark A Biggar @ 1995-04-19 0:00 UTC (permalink / raw) In article <dewar.798232482@gnat> dewar@cs.nyu.edu (Robert Dewar) writes: >yes, quite right: (one equivalence proof = two reduction proofs) >Ah well, difficult to type in accurate text books into a newsgroup :-) All true, but for the type of problems we have been discussing is usually sufficies to show that Problem X reduces to the Halting Problem and not vis-versa because we already know that the Halting Problem is unsolvable and that's what we are trying to show about Problem X. -- Mark Biggar mab@wdl.loral.com ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Mark A Biggar @ 1995-04-19 0:00 ` Robert Dewar 1995-04-19 0:00 ` Steve Tate 1 sibling, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-19 0:00 UTC (permalink / raw) Mark Biggar says: "All true, but for the type of problems we have been discussing is usually sufficies to show that Problem X reduces to the Halting Problem and not vis-versa because we already know that the Halting Problem is unsolvable" On the other hand, suppose we had already solved problem X, and then managed to reduce the halting problem to problem X. That would be quite interesting :-) ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-19 0:00 ` Mark A Biggar 1995-04-19 0:00 ` Robert Dewar @ 1995-04-19 0:00 ` Steve Tate 1 sibling, 0 replies; 76+ messages in thread From: Steve Tate @ 1995-04-19 0:00 UTC (permalink / raw) Mark A Biggar (mab@dst17.wdl.loral.com) wrote: > In article <dewar.798232482@gnat> dewar@cs.nyu.edu (Robert Dewar) writes: > >yes, quite right: (one equivalence proof = two reduction proofs) > >Ah well, difficult to type in accurate text books into a newsgroup :-) > All true, but for the type of problems we have been discussing is usually > sufficies to show that Problem X reduces to the Halting Problem and not > vis-versa because we already know that the Halting Problem is unsolvable > and that's what we are trying to show about Problem X. Be careful about what wording you use though. If you want to show that problem X is non-recursive (i.e., non-computable) then you only have to do one reduction. However, this is not an equivalence proof, and you should not be lulled into thinking that X and the Halting Problem are equivalent because they are both non-computable. Among the non-computable problem there are many "degrees" of non-computable functions, some harder in a very important way than others. In fact, the halting problem is one of the *easier* non-computable problems! -- Steve Tate --- srt@cs.unt.edu | "As often as a study is cultivated by narrow Dept. of Computer Sciences | minds, they will draw from it narrow University of North Texas | conclusions." -- John Stuart Mill, 1865. Denton, TX 76201 | ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? [not found] ` <cppD77Ex6.E77@netcom.com> [not found] ` <3mve9b$gaj@news.cais.com> [not found] ` <dewar.798172270@gnat> @ 1995-04-21 0:00 ` Robert I. Eachus 1995-04-21 0:00 ` Robert Dewar 2 siblings, 1 reply; 76+ messages in thread From: Robert I. Eachus @ 1995-04-21 0:00 UTC (permalink / raw) In article <dewar.798271681@gnat> dewar@cs.nyu.edu (Robert Dewar) writes: > On the other hand, given a formal definition of the language you > are compiling, it is at least conceptually feasible to prove that a > compiler gives an error message of *some* kind for any incorrect > program. Of course, as Robert knows well, if the language is non-trivial, such a compiler will be guarenteed to give an error message for some correct programs. (This corollary of Godels' proof scares lots of people, but shouldn't. A perfectly legitimate example of this sort of thing is for the compiler to run out of storage, or room in the symbol table, or whatever.) -- Robert I. Eachus with Standard_Disclaimer; use Standard_Disclaimer; function Message (Text: in Clever_Ideas) return Better_Ideas is... ^ permalink raw reply [flat|nested] 76+ messages in thread
* Re: What good is halting prob? 1995-04-21 0:00 ` Robert I. Eachus @ 1995-04-21 0:00 ` Robert Dewar 0 siblings, 0 replies; 76+ messages in thread From: Robert Dewar @ 1995-04-21 0:00 UTC (permalink / raw) " Of course, as Robert knows well, if the language is non-trivial, such a compiler will be guarenteed to give an error message for some correct programs." Robert does not "know this well", Robert Eachus and I have argued over his interpretation of Goedel's theorem in this context. I think his interpretation is completely bogus, and that this does not apply. Given a typical computer language, it is certainly possible to write a parser that is 100.(infinite zeroes) correct in its ability to diagnose syntactically correct programs. Of course, given an arbitrary size input, your compiler may require arbitrary amounts of memory. You may say "ah ha", there you go, a limitation, because I know perfectly well you don't have arbtirary amounts of memory, but by the same token, how can you present an arbitrary length program to the compiler in the first place. This is unuseful angels-on-pins stuff. I am not uncomfortable with this "consequence" of Goedel's theorem, because I do not accept that it applies in this case. ^ permalink raw reply [flat|nested] 76+ messages in thread
[parent not found: <3mo2j0$8e8@kaiwan009.kaiwan.com>]
* Re: Academic CS Losers? [not found] <3mo2j0$8e8@kaiwan009.kaiwan.com> @ 1995-04-20 0:00 ` Richard A. O'Keefe 0 siblings, 0 replies; 76+ messages in thread From: Richard A. O'Keefe @ 1995-04-20 0:00 UTC (permalink / raw) jmartin@kaiwan009.kaiwan.com (Jay M Martin) writes: >If Computer Science can't get industry to donate code, then it time >for Computer Science to do large projects themselves. I keep telling people how very impressed I am by the Icon project. Icon is an interesting programming language. Arizona have a larger installed user base than some commercial companies. They have ported Icon to a very wide range of architectures and operating systems. BUT to do something like this doesn't require just one very smart professor (Griswold) and good students; it requires a long-term commitment from the whole department and it requires $money$ to pay for the hardware and clerical support. I hope students who've worked on Icon are very much more employable; they deserve to be. But if you get calls from head-hunters saying "have you got any students who can program Windows below the API level? There's a lot of demand for that" (this really happened to me) it is rather discouraging. >Why is doing >large important software project demonstrating clean software >techniques so disparaged in CS? _Is_ it disparaged in CS? We'd do it like a shot if (a) we could do it without kicking a whole lot of important things out of the curriculum (including technical writing) that _are_ there. We're constantly trying to improve our course, but there is just so much time in an undergraduate degree and there is _so_ much we need to teach. (Like spelling and arithmetic. It's not just the US schools. TV has had the same effects everywhere.) (b) if it didn't frighten off potential students. When we were just _thinking_ about switching from Pascal to another language in first year, we got phone calls from schools saying "do that and we'll tell our pupils to go to elsewhere". I am not joking. We've switched to Ada. Great language. But I hope we survive the change. (c) the market for students who've done it were just a _bit_ bigger. Industry apathy isn't confined to the USA either. (For what it's worth, some of the research projects some of our staff work on _are_ clean commercial level software involving some graduate students.) We've switched to Ada because we _are_ interested in producing students who can write working code to spec (as well as understanding what they are doing). We'll consider _any_ suggestions to help achieve that goal. What should we be doing? >It >seems to me reasonable to require 3-6 quarter classes (2-4 semester) >of programming lab on a real project. I think the students would >learn alot. Empirical studies could be done with these labs. >Please tell me why this is not being done (I know there has got >to be a reason). There aren't 2-4 semesters spare. What do we kick out to make room? That's our problem. We're not teaching rocket science either. (Big-Oh is not rocket science. It is very very practical. Basically, it puts some detail on the motto "beware of solving toy problems".) >Why can't Computer Science answer the real questions like which >approach to software construction are optimal given which >circumstances? Fundamental questions like: Should programming >languages be more controlled/disciplined or more free/powerful? Questions about programming languages have a lot to do with psychology. Since people and problems differ, I'm afraid the answer is "sometimes they should and sometimes they shouldn't; it depends". Besides, where is it written that more controlled is the opposite of more powerful? Ada is _both_ more discplined _and_ more powerful than C. Again, software construction is mathematical, social, political, legal, and psychological as well as computational. Some academics _are_ trying to tackle these issues (not me). See for example the work on meta-modelling. A student here is working on meta-modelling of OOD. It's important. It's hard. >If >academia actually cared about teaching the latest software methods, >then I believe Ada would have immediately taken off at universities. As it happens, I learned about Ada at a University. I friend and I were even going to post a comment in the first general review about exceptions, but we found that someone else got there first. This was even before Ada 83. >They would have been out front on OO technology instead of eating >industry's dust. Where did SELF, Sather, Tethys, Emerald, and a lot of other good OOP come from? Industry? Nope. >Many years ago it seemed to me the academia was out >in front, now they have regressed to teaching C (talk about training). In the 90s, universities have to earn a living. When I was an undergraduate, the NZ government paid me to study. Nowadays that's a thing of the past. NZ and Oz governments charge students, and not small sums. Any student who can do a bit of arithmetic says "hmm, I am going to spend $X for Y years, instead of earning $Z. I had better earn at least ($X+$Z)*Y more than someone without a degree otherwise I will be losing money." In my case, even though my education was subsidised, the loss of income means that I won't break even (compared with someone who gets a job hacking visual basic) until I'm 50. This means that there is a *very* strong pressure from students "don't waste my time with things that won't directly help me get a well paying job". RMIT _has_ resisted the pressure to train people in C or C++ or whatever the fashion of the instant is (we do teach them whereabouts in the course and to the degree that it makes sense), but if we go _too_ far out in front it will ruin us. Specifically: we run a very real risk of being perceived by students and industry as "theoretical", "impractical", "out of touch" precisely *because* we have switched to Ada. If we spent a significant time on Eiffel, bye-bye students, bye-bye income. What it boils down to is that we can only afford to teach things that industry is willing to reward students for having learned. -- "The complex-type shall be a simple-type." ISO 10206:1991 (Extended Pascal) Richard A. O'Keefe; http://www.cs.rmit.edu.au/~ok; RMIT Comp.Sci. ^ permalink raw reply [flat|nested] 76+ messages in thread
end of thread, other threads:[~1995-04-21 0:00 UTC | newest] Thread overview: 76+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 1995-03-17 0:24 Should internet support software be written in Ada? Bill Brooks 1995-03-17 8:47 ` Anthony Shipman 1995-03-19 22:06 ` David Weller 1995-03-23 15:05 ` Theodore Dennison 1995-03-24 10:26 ` Fred J. McCall 1995-03-27 9:50 ` Robb Nebbe 1995-03-27 19:43 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Robert I. Eachus 1995-03-27 23:14 ` Arthur Evans Jr 1995-03-29 0:00 ` Dan 1995-04-01 0:00 ` Mike White 1995-04-04 0:00 ` Robert Dewar 1995-04-06 0:00 ` Theodore Dennison 1995-04-06 0:00 ` Norman H. Cohen 1995-04-07 0:00 ` Robert Dewar 1995-04-07 0:00 ` Tucker Taft 1995-04-07 0:00 ` Mike White [not found] ` <3ma7rt$smt@kaiwan009.kaiwan.com> [not found] ` <dewar.797514490@gnat> [not found] ` <3meunj$66u@felix.seas.gwu.edu> 1995-04-20 0:00 ` CS teachers who can't code their way outta a paper bag Richard A. O'Keefe 1995-03-27 14:24 ` Should internet support software be written in Ada? Theodore Dennison 1995-03-28 0:00 ` Robert Dewar 1995-03-28 9:32 ` Fred J. McCall 1995-03-29 0:00 ` Theodore Dennison 1995-03-29 0:00 ` Robert I. Eachus 1995-03-31 0:00 ` Theodore Dennison 1995-04-05 0:00 ` Wes Groleau 1995-04-07 0:00 ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Wes Groleau 1995-04-07 0:00 ` Robert Firth [not found] ` <D6qyv0.6Jv@nntpa.cb.att.com> 1995-04-19 0:00 ` Fergus Henderson 1995-04-19 0:00 ` Fred J. McCall 1995-04-19 0:00 ` George Haddad 1995-04-20 0:00 ` Mark A Biggar 1995-04-20 0:00 ` Bill Winn 1995-04-20 0:00 ` Robert Dewar 1995-04-20 0:00 ` State machines and Goto's (was Re: Sho Brian Hanson 1995-03-22 23:08 ` Should internet support software be written in Ada? Keith Thompson [not found] ` <dewar.798093453@gnat> 1995-04-20 0:00 ` What good is halting prob? Max Hailperin [not found] ` <dewar.798207931@gnat> [not found] ` <cppD78ywq.B31@netcom.com> [not found] ` <dewar.798240702@gnat> 1995-04-19 0:00 ` Problems with proofs Brian Harvey 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Steve Tate 1995-04-20 0:00 ` Apology to Steve Robin Rowe 1995-04-20 0:00 ` Problems with proofs Robert Dewar 1995-04-21 0:00 ` Robin Rowe 1995-04-21 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robert Dewar 1995-04-21 0:00 ` Larry Kahn [not found] ` <3n1fsv$lgd@butch.lmsc.lockheed.com> 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Garlington KE [not found] ` <3me1qs$n4a@theopolis.orl.mmc.com> [not found] ` <3mevmu$8an@felix.seas.gwu.edu> [not found] ` <3mh75i$8eu@rational.rational.com> [not found] ` <3mjihr$iqq@felix.seas.gwu.edu> [not found] ` <3mp20f$80t@kaiwan009.kaiwan.com> 1995-04-20 0:00 ` Academic CS Losers? Phillip Fanous 1995-04-21 0:00 ` Bill Winn [not found] ` <3mrv7h$3mq@larry.rice.edu> [not found] ` <3msnu4$6am@kaiwan009.kaiwan.com> [not found] ` <KUBEK.95Apr18213646@insage.gerii.insa-tlse.fr> [not found] ` <cppD792GC.1uI@netcom.com> 1995-04-20 0:00 ` Teaching OO/C++ Philip Machanick [not found] ` <cppD75t6F.47M@netcom.com> [not found] ` <EACHUS.95Apr17172831@spectre.mitre.org> [not found] ` <cppD77Ex6.E77@netcom.com> [not found] ` <3mve9b$gaj@news.cais.com> 1995-04-18 0:00 ` What good is halting prob? Jay M Martin 1995-04-19 0:00 ` Steve Tate 1995-04-20 0:00 ` Jay M Martin 1995-04-21 0:00 ` Steve Tate 1995-04-21 0:00 ` Ray Toal [not found] ` <cppD7880n.32B@netcom.com> 1995-04-19 0:00 ` Randolph Crawford 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 1995-04-20 0:00 ` Robert Dewar 1995-04-20 0:00 ` Robin Rowe 1995-04-21 0:00 ` Brian Hanson 1995-04-21 0:00 ` sxc [not found] ` <dewar.798172270@gnat> [not found] ` <cppD786FM.1u9@netcom.com> 1995-04-19 0:00 ` Mark A Biggar 1995-04-19 0:00 ` Richard Ladd Kirkham 1995-04-19 0:00 ` Robert Dewar 1995-04-20 0:00 ` Richard Ladd Kirkham 1995-04-20 0:00 ` Robert Dewar 1995-04-21 0:00 ` Mark A Biggar [not found] ` <dewar.798207364@gnat> [not found] ` <cppD78xMv.49w@netcom.com> 1995-04-19 0:00 ` Robb Nebbe [not found] ` <3n0ka7$b57@hermes.unt.edu> [not found] ` <dewar.798232482@gnat> 1995-04-19 0:00 ` Mark A Biggar 1995-04-19 0:00 ` Robert Dewar 1995-04-19 0:00 ` Steve Tate 1995-04-21 0:00 ` Robert I. Eachus 1995-04-21 0:00 ` Robert Dewar [not found] <3mo2j0$8e8@kaiwan009.kaiwan.com> 1995-04-20 0:00 ` Academic CS Losers? Richard A. O'Keefe
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox