Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!caen!ox.com!math.fu-berlin.de!dww From: dww@math.fu-berlin.de (Debora Weber-Wulff) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: Date: 15 Apr 91 17:17:45 GMT References: <1991Apr8.080931.23209@netcom.COM> <969@mgt3.sci.UUCP> <1991Apr12.073314.9415@netcom.COM> Sender: news@math.fu-berlin.de (Math Department) Organization: Free University of Berlin, Germany Lines: 44 mrs@netcom.COM (Morgan Schweers) writes: [bunch of stuff deleted] >It's my opinion that a product should work in ALL cases >before you ship it. It's also my opinion that this cannot be proven on >a systems programming level, since the variables are far too complex. >(As an example, we have one program which can't be used in a certain mode >with certain other programs, because they use memory in an odd way. Could >this have been proven to happen? Heck no. Could a 'formal' language prove >that we can successfully use the disk to swap in portions of our code during >runtime? Heck no. Am I wrong about this? Someone feel free to tell me of >a method that will tell me (just from looking at my source) that if I'm running > in memory, and another program swaps in to do some system checking >that there will be a memory conflict between the two. Assume, as is the normal >case, that I don't have the sourcecode to program X. Do you even think that >there is a language in which this *IS* possible? IMO, hell no.) Well, we're getting there. J Moore did a proof of correctness for an assembler, William Bevier did a proof for a small kernel, and Warren Hunt did one for the gate level implementation of a chip using the Boyer-Moore prover (see Journal of Automated Reasoning, December 1989). The prover - an obstinate, nagging proof checker that won't accept any nonsense - required the proof of all sorts of lemmata that get close to your problems. For example, it needed to be proven that the assembler program code could not modify itself during execution. I think a lot of people are just scared of formal methods because they smell like the m-word (*mathematics*), and they are afraid that they won't understand how to use them and might make fools out of themselves, so they just try and flame away in the hopes that formal methods will go away. "Wat de Buuer nit kunnt, dat frisst he nit" - (loose translation from the Low German: if the farmer doesn't recognize it, he won't eat it.) I quite agree with the opinions expressed in other postings: Use testing and/or proving as appropriate. -- Debora Weber-Wulff snail: FU Berlin, ZI Fachdidaktiken, Habelschwerdter Allee 45, W-1000 Berlin 33 email: weberwu@inf.fu-berlin.de, dww@math.fu-berlin.de