Some things change; some things don't.
The method of software development as applied in real-life development
situations has changed greatly during these 20 years. In the past,
we had "structured programming"; next, "complex
design" extended the field of view to the design stage; this
was followed by "structured design" and "structured
analysis". Now we have "object-oriented analysis/design/programming".
Of course, throughout this period, concepts such as "abstract
data types" and "information hiding" have formed
a consistent background for these developments, but in terms of
methods and/or notation, change has been going on to a considerable
extent much to the confusion and consternation of the software
engineer in the field.
On the other hand, some things don't change. For example: "formal
methods". From more than 20 years ago, this methodology has
been developing with the policy that software should be developed
on a sound mathematical basis. From around 20 years ago, this
methodology has been criticized by those who insisted that "mathematical
formalisms are not useful for real systems." However, by
now, the@"anti-formal method" stance has been shown
to be groundless. Formal methods have evolved from academic "toys"
to industrial-strength power tools, and their effectiveness of
application in real-life system development is proven.
To begin with, the notion that "mathematics isn't useful
for real systems" is a bit odd. Why? Since "programs
themselves are mathematical", perforce the logical conclusion
of such a position would be that "programs aren't useful
for real systems"!
With currently popular commercial/industrial programming languages,
while the resulting programs admittedly will not have a high-quality
mathematical underpinning, but they will be mathematical nonetheless.
Therefore, at some stage in the creation of a program, it is necessary
to model the@"mathematically indescribable" real world,
and on the basis of this model, to "describe it as a mathematical
system". Currently, this is most commonly performed at the
stage of programming.
But is this good practice? Clearly, it is far from ideal. Japanese
software is now just another type of pollution. The defects found
in software blighted with the Y2K problem are just one example
of this situation. If things are left at status quo, it is only
a matter of time before a great software-caused tragedy occurs.
Formal methods claim to perform the translation into mathematics
at the stage of requirements analysis. If this can be accomplished,
then with "stepwise refinement" using the almost 3000
transformation rules that have been discovered, it will be possible
to generate a program that by the programming stage is considerably
more accurate than that obtainable by previous methods. Further,
it is also possible to prove the validity of segments of this
process, and thus this method is well-suited for production of
high-reliability software. Already, such tool sets supporting
this methodology as B-Toolkit, CafeOBJ, RAISE Tool, VDMTools and
others are available, and are being applied in the configuration
of large-scale systems in Europe and America.
So, why aren't formal methods widely used in Japan?
The reason is simple. Because good textbooks in the Japanese language
are quite rare and university classes in formal methodologies
are few and far between, the result is a lack of Japanese formal
method experts, and only slight penetration into the various fields
of industry. In other words, the current situation resembles that
of 10 years ago regarding OO technology, and 15 years ago regarding
Unix.
In such circumstances, what needs to be done is clear.
First, the public needs to be warned that current circumstances
are such that a software-caused tragedy could occur at any time;
next, society's consciousness needs to be raised regarding the
position that production of high-reliability software is a matter
of duty rather than choice; good textbooks for formal methologies
must be written in Japanese; more venues and opportunities for
learning formal methods need to be provided; and the number of
experts in formal methodologies must be increased.
I propose that sigfm (Special Interest Group on Formal Methods)
be created within the venue of the Software Engineers' Association
(SEA).
sigfm will engage in the following activities based on the above-listed
goals:
In addition, ancient tradition dictates that such activities in
Japan require the accompaniment of food and drink; sigfm shall
not seek to scorn the wisdom of our ancestors.
Shin Sahara
translated by Edger M. Cooke
3 March, 2000@