HALLAM@physics.oxford.ac.uk ("Phillip M. Hallam-Baker") (05/21/91)
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
greeny@wotan.top.cis.syr.edu (Jonathan Greenfield) (05/21/91)
In article <4202.9105202128@prg.oxford.ac.uk> HALLAM@physics.oxford.ac.uk ("Phillip M. Hallam-Baker") writes: > >When they say >that occam programs may be proven correct they mean that an exact definition >of the occam language exists. I suspect that the assertion would not be made solely on the basis of a denotational semantic definition of the language. There must also be a complete set of proof rules that have been developed on the basis of those semantics, in order for one to reasonably claim that programs may be proven correct. >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. I disagree. Arguments that languages such as Pascal or Modula-2 are better than languages such as FORTRAN or COBOL are usually based upon syntax and structure. It is interesting to see Ada classified as an "old-fashioned" language when it is considerably more recent than Modula or Modula-2. It would appear that the distinction is between language that rely upon standard libraries, and those that do not. While, aesthetically, such a distinction may make a significant difference, it doesn't appear to make a whole lot of difference in terms of developing semantics and proof rules. It is probably more appropriate to classify occam along with FORTRAN, seeing as how they both lack modern data abstraction and recursion, not to mention their syntax... Likewise, for all its faults, it is probably more appropriate to classify Ada with Modula-2 and Pascal. Jonathan