Path: 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

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