Re: Formal methods?

[Marko Schuetz]

Atle,

From: Atle <trollet@skynet.be>
Subject: Formal methods?
Date: Fri, 01 Dec 2000 18:35:16 +0100

> Hello!
> Keeping quiet for a while, I feel it is time to ask (again?):
> What is the general attitude toward using formal methods (VDM-SL, Z, ...) in 
> the development of parts of the system?
> I guess you are all aware that in 20 years, no software will be built without 
> formal methods, just like nobody uses a hammer and saw
> (or whatever Henry Ford used :) to build a car anymore.
> Cars, planes, bridges, spacecraft, houses - everything is subject to rules of 
> engineering.
> Only software construction has until now 'escaped' - because it is a new 
> engineering discipline
> (programming is *NOT* an artform! :-)
> 
> In February I will take a course about large projects, with an OS as a case 
> study.
> There is one guy, teacher of formal methods, Georges Mariano 
> <georges.mariano@inrets.fr> who will specify Linux in Z or B, and with
> some help I might have a go at a Hurd subsystem.
> 
> But I will need help from someone who really knows the module, prefereably 
> the author or maintainer.
> And nothing will be 'obvious' or 'self-explanatory' - everything has to be 
> specified down to the most 'insignificant' detail, with
> domain specification, codomain (range), pre-conditions, post-conditions, 
> invariants for data and loops, reification from a high
> level of abstraction down to bit-level ... a BIG, BIG job!!!
> 
> Anyone interested?

I am interested. In particular I am interested in how close your
specification will get to the actual code, i.e. how do you bridge the
gap from the specification language to the implementation language. I
agree that in a not so distant future verification will be much more
widely used, but one obstacle on the way to this future is that once
you have a proof that your software has a particular property that
proof should be automatically verifiable without your intervention if
you only make a small change to the source. As long as you do not have
a formal semantics for the implementation language this is automation
not possible. 


Please, do keep me informed on any progress.
        Marko