🚀 go-pugleaf

CAMPBELL writes "-
>>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?
>>


"proven correct" in formal systems speak means that a program implements
it's specification.

The basic idea is quite simple - if you have a good idea of what you want
and you have a good idea of what your tools do it is possible to get a good
idea as to whether your program is what you want "correct".

Of course to have a chance of getting something exactly right you have to
know exactly what you want, and exactly what your tools do. When they say
that occam programs may be proven correct they mean that an exact definition
of the occam language exists. Because occam is a simple language this is
possible. Most computer languages are defined imprecisely using English,
occam may be defined exactly (here comp scientists start muttering the
cabalistic incantations denotational semantics, CSP ...). This is the basis
of the claim that modern languages such as occam, modula, (perhaps C - it
is small enough but the pointers screw things up) are better than old
fashioned languages such as FORTRAN, COBOL and ADA.

Of course all this only makes a difference if you originaly specified the
problem correctly (and precisely). Mathematical techniques exist for this
such as Z and VDM.

Also you need quite a lot of `glue' to hold everything together, Dijkstra's
wekest precondition calculus comes in here as do theorem checkers etc....

As you may have gathered this is a bit of a black art at present, the problem
is that a proof of program correctness tends to require an imense amount of
imensely tedious drudge work. Also most of the tools are under development
and few fit together in a usable way. The most frustrating thing is that
although a very large number of (often very similar) tools exist most are
unusable when you try to use them to solve real problems.

If you get the chance David May of Inmos has a talk he gives on proving
programs correct. The T800 floating point unit has been formally verified
using "formal methods" - principaly occam and Z.

Phill Hallam-Baker