Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!oravax!ian From: ian@oravax.UUCP (Ian Sutherland) Newsgroups: comp.software-eng Subject: Re: "Correct" IS UNDEFINED! Message-ID: <1315@oravax.UUCP> Date: 3 Feb 90 17:23:55 GMT References: <7598@hubcap.clemson.edu> <9630012@hpirs.HP.COM> <91033@linus.UUCP> <17142@duke.cs.duke.edu> <17504@joshua.athertn.Atherton.COM> <1306@oravax.UUCP> <17651@joshua.athertn.Atherton.COM> Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland) Organization: Odyssey Research Associates, Ithaca, New York Lines: 41 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