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