CAMPBELL@CC.USU.EDU (05/21/91)
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
Geraint.Jones@prg.oxford.ac.uk (Geraint Jones) (05/21/91)
> What does it mean when it is claimed that Occam programs can be proven > to be correct? We talk of a program being proved correct if there is a proof (in the usual sense that mathematicians use the word) that the program meets a specification. The specification will normally be a statement in mathematical terms about the inputs and outputs of the program, and perhaps the state of the machine. Often the proof will just be something informal, the way most mathematcians' proofs are really pretty informal -- but rigorous, which is to say that you could fill in the details if you really want to. The substance of the claim about occam, though, is that it is much easier to produce such proofs about occam programs than (say) C programs, because it is much easier to reason about what they do. For example, the absence of any shared variables in occam means that you can reason about the value of a variable by considering only the process which has write access to that variable. If variables could be shared, you would have to hedge every judgement about the variable with a side condition about there being nothing else anywhere else in the system that could affect the value of the variable. Imagine trying to do this in Fortran, or a C program using pointers (as if there were any that didn't use pointers). An assignment in occam just changes the variable being assigned to, nothing else. You don't need to know everything about the program in which it appears to know what the assignment does. That sort of thing means proofs can be modular, like the programs. All those Good Things. > I assume that it does *not* mean that the program will work for my > application. No, it just means that it meets the specification. There remains the problem of deciding whether a program that meets that specification is what you wanted. However, that is meant to be a much easier task, because the specification will in general be much simpler than the program. It will (ideally) be a crystalisation of your understanding of what you want, and uncluttered with details of how someone thought they could get a machine to do what you wanted. > I assume that it does *not* mean that the program is free of bugs. Of course! Well, sadly, not quite. It can help a lot, because you oughtn't to be able to produce a proof that a program which doesn't meet a specification does do so. Proofs, being constructed by mere mortals, are however no more nearly perfect than anything else we make. You can do a lot to improve your confidence in the correctess of a program, though. There is a fair chance that you won't make the same error in a proof as you did in the program, so you will catch a number of bugs that way. The proof should be much more readable than the program, so you ought to be able to get other people to catch more of your bugs that way. And if you are really lucky, you will be able to recruit the assistance of a mechanical proof checker. Programming is an engineering profession, and what all this stuff is about is improving your confidence in the correctness of a program by orders of magnitude. > Also has anyone actually used this advantage of Occam? Yes, of course. Real Programmers do it all the time. While you're writing your program, you should have in mind the shape of the proof of correctness. Indeed, Real Programmers do the proof first and fill in the program afterwards! If you want the classic example of where this stuff paid off, take the software floating point package for the T4 transputers, which is a really pretty ugly, and boring, bit of occam code. There is however very good reason to suppose that it really does meet the specification of IEEE floating point arithmetic, because it was written this way. The same techniques were used then to go on to the microcode of the T8 transputer's floating point arithmetic processor. (The bug in the first silicon T8s was introduced later...) g