Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!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: <50419@nigel.ee.udel.edu> Date: 11 Apr 91 15:57:10 GMT References: <1991Apr8.080931.23209@netcom.COM> <50097@nigel.ee.udel.edu> Sender: usenet@ee.udel.edu Organization: University of Delaware Lines: 59 Nntp-Posting-Host: snow-white.ee.udel.edu In article peter@ficc.ferranti.com (Peter da Silva) writes: >In article <50097@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: >> You can also write programs which could not possibly be implemented in >> C, even by Dan Bernstein :-). What more proof do you need? >This is as insane a claim as any of Dan's. If it's implementable in >principle it's implementable in C. It might take building another >language on top of C to make it convenient, but it's implementable. If you look closely at the complete post, you will notice that I never claimed that all LOTOS programs are implementable. For example, LOTOS very easily allows you to use integers and queues and such, and you must go out of your way to use integers mod 2^32 or bounded queues or whatever. Of course, programs which you write based on a LOTOS specification will not necessarily implement the full specification, but it is possible to determine where there will be problems. In practice, people write things like "every time you get a connection, either pick a new port or return an error." The specification says that it is possible to always pick a new port or always return an error. For different and hopefully obvious reasons, neither is practical. But the point of LOTOS is not the automatic implementation from the specification (use Estelle for that :-) but the concise and formal description of complex reactive behavior. >> How do you know Ada's validation suite tests all the semantics of Ada? >> Do you want to build SDI based on "I think so"? >Is there an alternative? How do you specify hardware and human actions >based on a formal language specification? I understand a CPU called "viper" has in some way been formally validated. Check out ACM architecture-oriented journals. 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. (The laws are enforced, so it really is formal.) LGS's are described in various Rutgers University tech reports. In any case, a formal semantics for Ada would allow you to know that the validation suite tested all parts of the compiler. These tests would not necessarily assure you that the compiler is correct, of course. Kind of like testing the implementation of a protocol by making sure that all transitions in the state machine fire at least once and wind up in the correct final state; without that, you don't even know if all the code is linked in, let alone correct. -- -- -- BTW, in reference to the FORTH-based NOVA chip: I can't find the reference, but that isn't suprising since most of my journals are in boxes in another state. I suspect I read about it in one of the ACM publications, probably ASPLOS. Definitely sometime around 1987 or 1988. -- 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 +=+=+ +=+=+ When you drive screws with a hammer, nails look better +=+=+