On Tue, 23 Jun 2009, Dave Korn wrote: > I'd guess there has to be some way in formal logic or propositional calculus > by which we could take descriptions such as Richard's above, and the > description of restrict semantics in the standard, and reduce them each to a > pile of propositions that we could feed into a theorem-proving system and get > it to prove they were identical.
Norrish's thesis <http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-453.pdf> formalised a subset of C90 in HOL, but I don't know what developments there have been in this area since 1998. It may not always be clear what the standard means, and I also quote Norrish: This ... tells us nothing about the quality of our semantics with respect to the original specification .... Better would be to have the specification of the semantics inspected by another individual who was both familiar with the fine details of the ISO standard, and the techniques of operational semantics. Unfortunately, such people are hard to find, which is rather an indictment of the divergence between theory and practice in computer science. Theorem proving systems have been successfully used for IEEE floating-point algorithms, where the intended semantics are more precisely defined and better understood. I believe that following the Pentium FDIV bug Intel now uses formal verification for the floating-point algorithms in its processors. -- Joseph S. Myers jos...@codesourcery.com
