Re: Denotational Semantics and Language Standards

Article View: comp.std.c

Article #895

#895

From: Doug Gwyn
Date: Fri, 10 Nov 1989 19:15

12 lines
1379 bytes

In article <1989Nov9.201125.8989@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes:
>Maybe.  Remember that "proved" and "disproved" should really read "claimed
>to be [dis]proved" -- only God can consistently write error-free proofs.
>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!

My favorite was an example in Dijkstra's classic "A Discipline of
Programming" where he claimed that he hadn't submitted his program
to operational testing since it had been created using a discipline
that guaranteed it would be correct.  Naturally, there were a couple
of bugs in it!

Technical Details

Message-ID: <11581@smoke.BRL.MIL>

Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!iuvax!purdue!haven!adm!smoke!gwyn

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>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!iuvax!purdue!haven!adm!smoke!gwyn
From: gwyn@smoke.BRL.MIL (Doug Gwyn)
Newsgroups: comp.std.c
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <11581@smoke.BRL.MIL>
Date: 10 Nov 89 19:15:05 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>
Reply-To: gwyn@brl.arpa (Doug Gwyn)
Organization: Ballistic Research Lab (BRL), APG, MD.
Lines: 12

Reply to Parent Message