Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!emory!gatech!bloom-beacon!eru!hagbard!sunic!mcsun!ukc!slxsys!ibmpcug!mantis!mathew From: mathew@mantis.co.uk (mathew) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: Date: 12 Apr 91 15:07:50 GMT References: <50419@nigel.ee.udel.edu> Organization: Mantis Consultants, Cambridge. UK. Lines: 62 new@ee.udel.edu (Darren New) writes: > In article peter@ficc.ferranti.com (Peter da Sil > > 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. This is correct. The Viper CPU is a relatively simple CPU design; it was necessary to keep it so in order to make it validatable. The formal proof system for hardware is based around the language ML; you specify the actions of various elements of the design, and the system uses inference rules to construct a formal proof that the design is correct (or incorrect :-) There are still a number of problems with proving hardware correctness. For example, it is difficult to codify the behaviour of transistors accurately. Most transistor models either make too many assumptions to be generally applicable, or are too complicated to be tractable using automated proof methods. It is also the case that the proof is only as good as the information put in at the start. If what you say the hardware is does not match the actual chip layout, your proof is useless. In spite of this, formal verification of hardware is useful, and research continues. If people are interested I could dig out some examples of hardware verification. I think they are working on Viper II, which will be a slightly more useful chip (i.e. one which you might actually want to build into something more complicated than a toaster). > 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. The problem is that most powerful and expressive languages have complicated and messy formal semantics. As soon as you start allowing pointers, goto statements, side-effects like x = y++ and the like, your semantics become horribly complicated or even impossible to formulate. I'm personally unconvinced by denotational semantics; it seems to be a way of spraying some maths over the problem to make it look like a formal proof of something, and I can't see that big an advantage over operational semantics. Still, it wasn't my favourite course by any means, and I may have been misled. Certainly operational semantics is useful as a way of expressing what a particular bit of code does in a much less ambiguous and more tractable way than is possible via an English-language description. > 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. It's called the NOVIX. mathew -- If you're a John Foxx fan, please mail me!