From: William Rutiser <wruyahoo05@...>
Date: 2010-04-28T05:04:22+09:00
Subject: Re: Formal methods

Robert Dober wrote:
> On Tue, Apr 27, 2010 at 6:42 PM, Bernhard Brodowsky
> <brodowsb@student.ethz.ch> wrote:
>   
>> Robert Dober wrote:
>>     
> <snip>
>   
>> Maybe I'll do my bachelor thesis on this. :D
>>     
> 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