Atle,
From: Atle <[EMAIL PROTECTED]>
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
><[EMAIL PROTECTED]> 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
_______________________________________________
Help-hurd mailing list
[EMAIL PROTECTED]
http://mail.gnu.org/mailman/listinfo/help-hurd
