Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!udel!ee.udel.edu From: new@ee.udel.edu (Darren New) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: <50577@nigel.ee.udel.edu> Date: 12 Apr 91 21:52:31 GMT References: <50419@nigel.ee.udel.edu> Sender: usenet@ee.udel.edu Organization: University of Delaware Lines: 53 Nntp-Posting-Host: snow-white.ee.udel.edu In article peter@ficc.ferranti.com (Peter da Silva) writes: >In article <50419@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: >Well, you said there wasn't currently a compiler available for it. That >doesn't say the same thing as "it's not implementable". I said "Can you compile it? No." if you want to be picky :-) >> Of course, programs which you write based on a LOTOS >> specification will not necessarily implement the full specification, >... and may be written in C as well as anything ... No argument. Of course, if you *do* write it in LOTOS (the subset that you could compile) then you can be sure it implements what was specified. >> I understand a CPU called "viper" has in some way been formally validated. >Fine. How about the rest of the system (up to and including launch vehicles, >ordnance, sensors, etc...)? Probably not. What's your point? I'm not trying to say that formal specifications can prevent you from needing to test anything. I'm merely saying that they *help*. Tastes great, less filling. >> Also, law-goverend systems >> can formally specify the ways in which people are allowed to interact >> with the system, including the ways in which they are allowed to change >> the code and the laws themselves. >I see, the formal specification rules out infiltrating the U.S. with small >nuclear devices hidden in Ford Econoline vans? Well, the quality of this post is certainly not up to the standards I've come to expect from your posts. If you forgot the :-)'s then I understand. I can't imagine what blowing up the computer has to do with whether there are bugs in a program due to misunderstanding of what the compiler is supposed to support. It's also possible to have the police arrest and beat to death the programmers; does that mean we shouldn't have laws? Sorry for mentioning these other formal systems. It was my impression that you might be interested in hearing about something you might not know about, rather than pointless flamage. Geez. >Peter da Silva. `-_-' peter@ferranti.com -- Darren -- --- Darren New --- Grad Student --- CIS --- Univ. of Delaware --- ----- Network Protocols, Graphics, Programming Languages, FDTs ----- +=+=+ My time is very valuable, but unfortunately only to me +=+=+