Re: Should internet support software be written in Ada?

Re: Should internet support software be written in Ada?

[Bill Brooks]

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"

Re: Should internet support software be written in Ada?

[Anthony Shipman]

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

Re: Should internet support software be written in Ada?

[David Weller]

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   :-)

Re: Should internet support software be written in Ada?

[Theodore Dennison]

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.

Re: Should internet support software be written in Ada?

[Fred J. McCall]

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.

Re: Should internet support software be written in Ada?

[Robb Nebbe]

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

State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Robert I. Eachus]

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...

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Arthur Evans Jr]

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

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Dan]

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

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Mike White]

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  * 
***************************************************************************

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Robert Dewar]

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.

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Theodore Dennison]

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)

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Norman H. Cohen]

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

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Robert Dewar]

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.

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Tucker Taft]

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.

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Mike White]

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  * 
***************************************************************************

Re: CS teachers who can't code their way outta a paper bag

[Richard A. O'Keefe]

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.

Re: Should internet support software be written in Ada?

[Theodore Dennison]

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.

Re: Should internet support software be written in Ada?

[Robert Dewar]

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 :-)

Re: Should internet support software be written in Ada?

[Fred J. McCall]

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.

Re: Should internet support software be written in Ada?

[Theodore Dennison]

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)

Re: Should internet support software be written in Ada?

[Robert I. Eachus]

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...

Re: Should internet support software be written in Ada?

[Theodore Dennison]

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"

Re: Should internet support software be written in Ada?

[Wes Groleau]

>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 ...

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Wes Groleau]

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.

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Robert Firth]

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;
	...

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Fergus Henderson]

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

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Fred J. McCall]

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.

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[George Haddad]

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?

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Mark A Biggar]

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

Re: State machines and Goto's (was Re: Sho

[Brian Hanson]

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

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Bill Winn]

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.

Re: State machines and Goto's (was Re: Should internet support software be written in Ada?)

[Robert Dewar]

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!

Re: Should internet support software be written in Ada?

[Keith Thompson]

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'.

Re: What good is halting prob?

[Max Hailperin]

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.

Re: Problems with proofs

[Brian Harvey]

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"!

Re: Problems with proofs

[Robert Dewar]

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.

Re: Problems with proofs

[Robin Rowe]

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!

Re: Problems with proofs

[Robert Dewar]

><< 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!)

Re: Problems with proofs

[Robin Rowe]

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!

Re: Problems with proofs

[Robert Dewar]

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 ...

Re: Problems with proofs

[Robert Dewar]

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.

Re: Problems with proofs

[Steve Tate]

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               | 

Re: Apology to Steve

[Robin Rowe]

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!

Re: Problems with proofs

[Larry Kahn]

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)

Re: Problems with proofs

[Robin Rowe]

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!

Re: Problems with proofs

[Robin Rowe]

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!

Re: Problems with proofs

[Garlington KE]

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.

Re: Academic CS Losers?

[Phillip Fanous]

: (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.

Re: Academic CS Losers?

[Bill Winn]

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.

Re: Teaching OO/C++

[Philip Machanick]

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

Re: What good is halting prob?

[Jay M Martin]

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

Re: What good is halting prob?

[Steve Tate]

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               | 

Re: What good is halting prob?

[Jay M Martin]

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

Re: What good is halting prob?

[Steve Tate]

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               | 

Re: What good is halting prob?

[Ray Toal]

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

Re: What good is halting prob?

[Randolph Crawford]

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

Re: What good is halting prob?

[Robert Dewar]

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.

Re: What good is halting prob?

[Robin Rowe]

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!

Re: What good is halting prob?

[Robert Dewar]

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.

Re: What good is halting prob?

[Robin Rowe]

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!

Re: What good is halting prob?

[Brian Hanson]

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

Re: What good is halting prob?

[sxc]

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
  

Re: What good is halting prob?

[Mark A Biggar]

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

Re: What good is halting prob?

[Richard Ladd Kirkham]

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

Re: What good is halting prob?

[Robert Dewar]

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).

Re: What good is halting prob?

[Richard Ladd Kirkham]

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

Re: What good is halting prob?

[Robert Dewar]

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!

Re: What good is halting prob?

[Mark A Biggar]

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

Re: What good is halting prob?

[Mark A Biggar]

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

Re: What good is halting prob?

[Robert Dewar]

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 :-)

Re: What good is halting prob?

[Steve Tate]

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               | 

Re: What good is halting prob?

[Robb Nebbe]

: 
: 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

Re: What good is halting prob?

[Robert I. Eachus]

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...

Re: What good is halting prob?

[Robert Dewar]

"   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.

Should internet support software be written in Ada?

[Bennett, Chip (KTR) ~U]

I just read an interesting article in Federal Computer Week.  The article,
titled "Energy group uncovers hole in Web software" is rather old (Feb 20),
so if this ground has already been covered, I apologize for rehashing it.

The article points out that the NCSA's httpd version 1.3 has a flaw where a
hacker might be able to overflow internal buffers and gain root access.

Point 1:  Didn't we already go through this several years back with a UNIX
mail server that had a similar problem?  Any history buffs remember that
one?

Point 2:  I going to make a huge leap here and assume that httpd is written
in C.  I'd bet that if the software had been written in a constraint
checking language like Ada, the problem would not have occurred.  Comments?

Chip Bennett

Re: Should internet support software be written in Ada?

[Vladimir Vukicevic]

In article <2F5B780E@SMTPGATE2.STRATCOM.AF.MIL> "Bennett, Chip (KTR)
~U" <BennettC@J64.STRATCOM.AF.MIL> writes:
> I just read an interesting article in Federal Computer Week.  The
> article, titled "Energy group uncovers hole in Web software" is
> rather old (Feb 20), so if this ground has already been covered, I
> apologize for rehashing it.
>
> The article points out that the NCSA's httpd version 1.3 has a flaw
> where a hacker might be able to overflow internal buffers and gain
> root access.
>
> Point 1: Didn't we already go through this several years back with
> a UNIX mail server that had a similar problem?  Any history buffs
> remember that one?

I believe nearly every widely-used unix tool has had this problem. I
know that finger had it, sendmail had it, and I'm sure many, many more
had (or still have?) this same problem.

> Point 2: I going to make a huge leap here and assume that httpd is
> written in C.  I'd bet that if the software had been written in a
> constraint checking language like Ada, the problem would not have
> occurred.  Comments?

Yes and no. It depends on where the overrun occurs. If it overruns
while, say, reading from a socket (via a syscall), then it could not
be prevented by using Ada or any other language because all the
procedure which actually stuffs bytes into the buffer has is a
System.Address (in Ada terms). If, however, the overrun occurs in user
code, i.e. copying from one string to another (maybe they're actually
reading in 256 bytes at a time, and then just appending them to
another buffer until there's no more data), then Ada would have
probably raised Constraint_Error on this operation.

There is no reason why unix/internet tools shouldn't be written in
Ada. Perhaps the most persuasive argument against doing so is that,
sadly, the majority of unix systems do not have an Ada compiler, while
they probably have a C compiler. Hopefully GNAT will change this; I've
already convinced a few people who, according to them, have no
intention of ever writing in Ada to install gnat on their systems just
in case something "truly cool" is released in Ada95. I think they're
still waiting to use the compiler.

	- Vladimir