Article View: comp.std.c
Article #892Re: Denotational Semantics and Language Standards
From: T. William Wells
Date: Fri, 10 Nov 1989 18:57
Date: Fri, 10 Nov 1989 18:57
15 lines
1352 bytes
1352 bytes
In article <1989Nov9.201125.8989@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes:
: Certainly human mathematicians and program-verification people don't, as
: witness quite a few embarrassing errors in formally-refereed published
: papers purporting to be demonstrations of how to verify programs!
:
: A formal definition of C would inevitably be large and messy, especially
: given the many places where C refuses to promise how the machine behaves.
: I suspect that proving theorems from it would not be a simple exercise.
Which leads us to: we finally would have a real use for all those
automatic theorem provers! 1/2 :-)
---
Bill { uunet | novavax | ankh | sunvice } !twwells!bill
bill@twwells.com
Technical Details
Message-ID:
<1989Nov10.185759.8031@twwells.com>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!wuarchive!cs.utexas.edu!uunet!twwells!billReferences:
<11065@riks.csl.sony.co.jp> <2727@cbnewsl.ATT.COM> <11477@smoke.BRL.MIL> <11081@riks.csl.sony.co.jp> <11555@smoke.BRL.MIL> <1989Nov8.222632.699@algor2.algorists.com> <1989Nov8.225008.793@algor2.algorists.com> <1989Nov9.201125.8989@utzoo.uucp>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!wuarchive!cs.utexas.edu!uunet!twwells!bill From: bill@twwells.com (T. William Wells) Newsgroups: comp.std.c Subject: Re: Denotational Semantics and Language Standards Message-ID: <1989Nov10.185759.8031@twwells.com> Date: 10 Nov 89 18:57:59 GMT References: <11065@riks.csl.sony.co.jp> <2727@cbnewsl.ATT.COM> <11477@smoke.BRL.MIL> <11081@riks.csl.sony.co.jp> <11555@smoke.BRL.MIL> <1989Nov8.222632.699@algor2.algorists.com> <1989Nov8.225008.793@algor2.algorists.com> <1989Nov9.201125.8989@utzoo.uucp> Organization: None, Ft. Lauderdale, FL Lines: 15