proving programs correct

Article View: comp.sys.transputer

Article #1679

Back to comp.sys.transputer Previous Next

#1679

From: CAMPBELL
Date: Mon, 20 May 1991 18:17

19 lines
1024 bytes

I sent this out a little while ago, but I didn't get any response.
I may have posted it wrong, so I am doing it differently this time.

What does it mean when it is claimed that Occam programs can be proven
to be correct? Does it only mean that they match the syntax of the
language?

I assume that it does *not* mean that the program will work for my
application.
I assume that it does *not* mean that the program is free of bugs.

Am I correct? If so what does it actually accomplish?

Also has anyone actually used this advantage of Occam?

Thanks

Russell Anderson
email: campbell@cc.usu.edu

Technical Details

Message-ID: <71DAE629A3DF03B4F9@cc.usu.edu>

Path:

arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!caen!uwm.edu!linac!att!ucbvax!CC.USU.EDU!CAMPBELL

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!caen!uwm.edu!linac!att!ucbvax!CC.USU.EDU!CAMPBELL
From: CAMPBELL@CC.USU.EDU
Newsgroups: comp.sys.transputer
Subject: proving programs correct
Message-ID: <71DAE629A3DF03B4F9@cc.usu.edu>
Date: 20 May 91 18:17:00 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The Internet
Lines: 19