Article View: comp.ai
Article #8647Re: Reasons why you don't prove your programs are correct
From: David H. West
Date: Mon, 08 Jan 1990 14:55
Date: Mon, 08 Jan 1990 14:55
17 lines
1166 bytes
1166 bytes
In article <25728@cup.portal.com> Nagle@cup.portal.com (John - Nagle) writes: > I once headed a group of five people that produced a verifier for >a dialect of Pascal. It worked, but it was too hard to use to be used >by most programmers. It's painfully difficult to convince a mechanical >theorem prover that your program is correct. I think that "most programmers" have never had access to a verifier, even a "hard to use" one. Are there any free verifiers out there? (*) -David West dhw@iti.org (*) I expect the number of available free verifiers to be so small that I don't want to discourage replies by imposing restrictions concerning language, etc. I'd be glad if the expectation were wrong.
Technical Details
Message-ID:
<4760@itivax.iti.org>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!sharkey!itivax!dhwReferences:
<7578@hubcap.clemson.edu> <25728@cup.portal.com>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!sharkey!itivax!dhw From: dhw@itivax.iti.org (David H. West) Newsgroups: comp.ai Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <4760@itivax.iti.org> Date: 8 Jan 90 14:55:34 GMT References: <7578@hubcap.clemson.edu> <25728@cup.portal.com> Reply-To: dhw@itivax.UUCP (David H. West) Organization: Industrial Technology Institute Lines: 17