Robert said:
To re insist on the complexity of the thing, PhD you mean?
R.
"Formal Methods" has meant different things to different people.
One aspect of the difference is what is to be proven. The general idea
is that some post-condition of the program's execution is to be proven.
Its not easy to write a formal post-condition for, say, an execution of
Internet Explorer. On the other hand it may be possible to specify the
effect of some of IE's subroutines.
Another aspect has to do with the completeness of the proof( and
specification ). For example, is it sufficient to prove that a program
gives the right answer if it doesn't blow up or fail to terminate? Do
you need to prove those things for some pre-specified range of inputs?
Do the numbers stay inside certain hardware limits? Do numerical
round-off errors have to be considered? etc. Perhaps you can do the
proof for an abstraction of the problem, one that ignores storage
representations and other machine artifacts. Do what extent do you need
to prove the real program matches the abstraction?
A third aspect is who or what does the work. Is some tool supposed to
figure out the entire proof? or is it supposed to just check a proof
supplied by a programmer?
Fourth, does the formal method apply to an arbitrary program or only one
composed in certain limited ways?
My experience, since encountering Edsger Dijkstra circa 1970, is that it
is practical to apply his methods to some programs. I wrote the array
manipulating code for a language interpreter that way. The program was
in carefully hand optimized C, and the proofs asserted that all the
pointers were pointing where they were supposed to.
But remember that Dijkstra's method is to write the program so that it
can be proven -- almost a proof first technique.
The program text contains the assertions that must hold after each
statement. If you can't write the assertion, and prove it follows from
previous assertions, you can't write the statement. Note that this is an
extremely oversimplified description.
What I found was that the experience of learning to program this way had
a major effect on all my subsequent programming, even when I was not
explicitly writting down the proof steps.
Note that the details of such proofs tend to be very tedious and most of
the things to be proven are pretty trivial. What is not trivial is
breaking larger goal into such trivial steps.
I am no longer, and haven't been for a long time, in contact with
computer science education. In particular I don't know how much of this
is a standard part of the curriculum and how much as been discarded as
not commercially applicable.
In summary, there are at least semi-formal things that can be done and
it is very beneficial to practice doing them.
-- Bill Rutiser
