crm@romeo.cs.duke.edu (Charlie Martin) (02/01/90)
In article <17504@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes: >> = crm@cs.duke.edu (Charlie Martin) writes: ># = munck@chance.UUCP (Robert Munck) writes: > >> Oh, crap. I'm sorry, but this is simply the single most assinine >> argument that I've seen proposed. Never in twenty years of software >> engineering have I seen a system where the question "does it work?" was >> undefined. Sometimes it's POORLY defined, sometimes the definition >> turns out to have contradictions, sometimes it turns out to be vacuous, >> but all of them have some statement of the expected behavior. > >The second part of you paragraph suggests that the first part of it is >just wishful thinking. I have seen definitions of software behavior >which are poor, vacuous, contradictions, and incorrect. What I have >not seen is a definition which was reasonably correct and which could >be used as the input to a software verification system, even a human >one. It just suggests that I can understand the difference between Not defined at all and badly defined. Can you? Or is this a straw man? > ># I'm afraid that belief that we will someday be able to prove our ># largest, most important programs correct has become one of my tests of ># native intelligence, along with belief in astrology and support of the ># flag-burning amendment. > >I would consider it a better measure of optimism and lack of real world >experiance. This is what is called "dick measuring." So, okay, whip it out. Let's see your CV/resume, and we'll compare it to mine. We can start with date of first professional programming job: mine was 31 October 1969. > >#ifdef PERSONAL_ATTACK > >If you go back through the "programs can be proven" thread, I think you >will find that 80-90% of the people who post in defence of proving >programs correct post from academic sites. You will also see that 80-90% >of the people who attack this idea post from commercial sites. >I do not think this is pure chance. Okay, we can play this game too. I'll just note that a friend left Atherton because she was tired of trying to sell or describe systems based on programs where no one could be bothered to write designs or specifications at all. > >#endif > Now that we've gone through the obligatory male-dominance nonsense, tell me: what is it that you object to in technology that IN INDUSTRIAL USE (see the cleanroom references) resulted in extremely low defect rates? stupid postnews program Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)
joshua@athertn.Atherton.COM (Flame Bait) (02/02/90)
> = ian@oravax.odyssey.UUCP (Ian Sutherland) writes: % = joshua@Atherton.COM (Flame Bait) % [I talk about seeing many bad definitions of software behavior, and no % good ones.] >If you're talking about systems like SDI, I agree to a certain extent. >Most of the attempts I've seen to say what such large systems should do >are as bad as you say. I think the difference is that I think it is impossible to make good defintions, while you think it is possible, it just has not been done yet. Why do you think it is not possible to specify SDI, but it is possible to specify AT&T's telephone system or a large database application, or an ADA compiler? >I will say that I've seen some reasonably >generic definitions of both fault tolerance and computer security >which are both reasonable and sufficiently precise to be input to a >human or mechanical software verification system. Yes, but these are both relatively narrow fields of interest. You might be able to prove facts about these limited domains, but I do not believe that this will translate very well to general systems. I think there is a big difference between looking at one aspect of a program as opposed to looking at the whole thing. Especially when the aspect is well defined like security or recovery. % #ifdef PERSONAL_ATTACK % If you go back through the "programs can be proven" thread, I think you % will find that 80-90% of the people who post in defence of proving % programs correct post from academic sites. You will also see that 80-90% % of the people who attack this idea post from commercial sites. % I do not think this is pure chance. % #endif >Was this really necessary Mr. Levy? Did it serve some important >purpose? It was not required for my argument. That is why I put it at the end of my posting, with special warning markers. I added it because I was surprized at how true it was. Usually in these discussions there is an even distribution of people on each side of the discussion. I was suprized at how lopsided this discussion was. Does it serve some purpose? I do not know. It is an interesting fact. Most people (who have emailed me) have interpreted it as some sort of attack on academics, which it was not supposed to be. Joshua Levy joshua@atherton.com home:(415)968-3718 {decwrl|sun|hpda}!athertn!joshua work:(408)734-9822
crm@romeo.cs.duke.edu (Charlie Martin) (02/02/90)
In article <13211@cbnewsc.ATT.COM> lgm@cbnewsc.ATT.COM (lawrence.g.mayka,ihp,) writes: >In summary, then: > >a) Requirements are somewhat relative. If customers really need >or want a product, they aren't going to let textbooks stand in >their way. Conversely, mere fulfilment of textbook requirements >is no guarantee that customers will buy your product. > >b) Market needs and wants change continually. A development >process that attempts to "freeze" requirements may put out >products that are obsolete the day of their introduction. > > > Lawrence G. Mayka > AT&T Bell Laboratories > lgm@ihlpf.att.com > >Standard disclaimer. Sure, sure. But there's a big difference (which I've noted more than once) between "meets requirements" and "the requirements really describe what is needed". But you have to look at it sort of like a contract: if you contract with me to build a system that meets a certain collection of requirements, and I do so, then the system must be correct. If it turns out you wanted another system, then I can build that too; what I can't do is read your mind. On the other hand, what we really want is satisfied customers; there has to be some way to pry from the customer or client what they *really* want, make sure it is feasible, and then delvier it with high certainty that what you deliver is what was finally agreed upon. The domain of verification is this second: give a specification and I can mathematically argue with great certainty that I have built it. I don't know the solutino to the first; the solution that appears best is incremental development and prototyping. It isn't easy. I don't think it will ever be easy. But all verification promises is to increase the trust in the realization meeting the specification. Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)
crm@romeo.cs.duke.edu (Charlie Martin) (02/02/90)
In article <13212@cbnewsc.ATT.COM> lgm@cbnewsc.ATT.COM (lawrence.g.mayka,ihp,) writes: > >An addendum to my previous posting: > >The lion's share of telecom switching system development is not >usually the construction of entirely new products, but the >addition of new functionality to the existing product line. Thus, >the well-understood, textbook requirements have often already been >met. Developers of new, innovative features do not always have >the luxury of firm, consistent requirements agreed upon throughout >the industry. > I don't think I understand this. I recognize that new features, not extensions to new peripherals or additions of things like nail-up connections to existing switches, nmay not have firm requirements at the time they are proposed. But do they not have to meet standards set through Bellcore before they can be integrated into the network. It was certainly my impression that Northern Telecom/BNR had to do this. Doesn't AT&T? Should Mean Judge Green know about this? Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)
crm@romeo.cs.duke.edu (Charlie Martin) (02/02/90)
In article <13212@cbnewsc.ATT.COM> lgm@cbnewsc.ATT.COM (lawrence.g.mayka,ihp,) w rites: > >An addendum to my previous posting: > >The lion's share of telecom switching system development is not >usually the construction of entirely new products, but the >addition of new functionality to the existing product line. Thus, >the well-understood, textbook requirements have often already been >met. Developers of new, innovative features do not always have >the luxury of firm, consistent requirements agreed upon throughout >the industry. > I don't think I understand this. I recognize that new features, not extensions to new peripherals or additions of things like nail-up connections to existing switches, nmay not have firm requirements at the time they are proposed. But do they not have to meet standards set through Bellcore before they can be integrated into the network. It was certainly my impression that Northern Telecom/BNR had to do this. Doesn't AT&T? Should Mean Judge Green know about this? Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)
crm@romeo.cs.duke.edu (Charlie Martin) (02/02/90)
In article <39400060@m.cs.uiuc.edu> render@m.cs.uiuc.edu writes: > >No one (except maybe you) thinks that "proving a program correct" means >proving absolutely, positively that there is not a single (no, not even >one) error in a program. Would that this were true. This is, unfortunately, just about exactly what I've spoken of as "Hoare's Folly." Hoare's argument for it depends on his (usually implicit) assumption that the only REAL program is the mathematical argument written on paper; he explicitly ignores executino concerns. Unfortunately he also makes the assumption the the True and Good Programmer will never make mistakes. Thus the presumption (and ghod is it presumptive!) that proven programs need not be tested. If this were better recognized, perhaps Fetzer's Dilemma would have been recognized as the straw man it really is. Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)
ian@oravax.UUCP (Ian Sutherland) (02/04/90)
In article <17651@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes: [quoting me] >>If you're talking about systems like SDI, I agree to a certain extent. >>Most of the attempts I've seen to say what such large systems should do >>are as bad as you say. > >I think the difference is that I think it is impossible to make good >defintions, while you think it is possible, it just has not been done >yet. Why do you think it is not possible to specify SDI, but it is >possible to specify AT&T's telephone system or a large database application, >or an ADA compiler? I don't think it's impossible to specify SDI, as I think is pretty clear from the text of mine that you quoted. I said I agree with you TO A CERTAIN EXTENT, and that most of the attempts I'VE SEEN are bad. This doesn't mean that I think that all possible attempts are bad. I think there's a problem with the way you state our difference of opinion. You state as a disagreement about whether the following statement is true or false: "It is possible to specify SDI." It's not clear what this means though. Does it mean "it is possible to specify SOMETHING about SDI that we want to be true" or "it is possible to specify EVERYTHING about SDI that we want to be true"? If the former, then yes, I believe the statement is true. I don't know whether you agree or not. If the latter, I frankly don't CARE whether it's true or false, and I would venture to say that most people in verification would say the same. Verification aims to prove that programs have desirable properties. It does not necessarily aim to prove that a program has ALL the properties that ANYONE considers desirable, if for no other reason than that for many programs you'll be able to find two people whose desires for the program are logically inconsistent. -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur
lgm@cbnewsc.ATT.COM (lawrence.g.mayka) (02/05/90)
In article <17271@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes: >I don't think I understand this. I recognize that new features, not >extensions to new peripherals or additions of things like nail-up >connections to existing switches, nmay not have firm requirements at the >time they are proposed. But do they not have to meet standards set >through Bellcore before they can be integrated into the network. It was The Regional Bell Operating Companies (RBOCs) may or may not wait for a Bellcore standard before purchasing new features, depending on factors such as market demand. Keep in mind that Bellcore is owned by the RBOCs and exists to serve them, not the other way around. A Bellcore standard is a technical recommendation to the RBOCs, not an imposed requirement. The international switching system market is even less regimented. International telecommunications standards focus primarily on interconnectibility, not feature offerings. Each country's PTT often has its distinctive notion of what services its subscribers need and want. Lawrence G. Mayka AT&T Bell Laboratories lgm@ihlpf.att.com Standard disclaimer.