Why Formal Methods?

J.N. Oliveira

The traditional classification of software packages as numerical or non-numerical (and in the latter case as either symbolic or data processing) has become obsolete with the advent of powerful computing devices which can easily accommodate hybrid applications on multiple platforms. (For example, a popular tool such as AutoCAD (TM) can be regarded as numerical on its graphical processing side, symbolic if AutoLISP (TM) is taken into account or even data oriented with respect to the information model which supports drawing structuring and management.)

There is, however, a substantial difference in nature between the numerical and non-numerical kinds of software. While the former has a strong support by centenary mathematical disciplines (such as the differential/integral calculi, numerical analysis, analytical geometry, statistics etc. ), the application of which is only limited by the need to finitely approximate real numbers modelling continuous entities such as space and time, the latter is usually designed by mere intuition in an ad hoc, trial and error style. (The apparent unability to produce defect-free software and the permanent need to maintain ill software led to the identification of a so-called software crisis since the 1960's, which structured programming of the 1970's and object-oriented programming of the 1980's have failed to completely solve.)

Why is this happening? Is it because there is no such mathematical support for non-numerical software design?

The answer is negative. In fact, non-numerical software can be formalized by disciplines such as abstract algebra, discrete mathematics and formal logic. However, these are rarely found in traditional engineering curricula, which are too much concerned with the mathematics of continuity to leave room for the mathematics of discreteness. Conventional engineers are thus bad software designers. However, many curricula on software engineering have been updated with the missing background. And so-called Formal Methods for software production are emerging everywhere among much other literature available) albeit slow to be adopted by industry.

The main target of the formal methods trend is to drive software production into good engineering standards. As a rule, these methods split software production into a specification phase, in which a mathematical model is built of the contractor requirements, followed by an implementation phase in which such model is somehow converted into a runnable software artifact. Relatively recent advances in formal method research show that implementations can be effectively calculated from specifications. So, in a sense, software technology is becoming a mature discipline in its (however late) adoption of the ``universal problem solving'' strategy which one is taught at school:

the sophistication of which is only dependent upon the underlying mathematics --- from simple arithmetics at primary school to systems of liner equations, then to differential/integral equations and now, in software calculi, to systems of (recursive) equations on domain spaces.

The introduction of mathematics and algebraic calculi in software enginneering appears to be a natural evolution, when compared with the historical development of the scientific bases for other engineering areas (eg. civil and mechanical engineering etc.) which, some centuries ago, started omitting complicated geometrical proofs in favour of algebraic reasoning.

Roughly speaking, this evolution may be sketched as follows:

The reader is left with the following quotation by a Portuguese mathematician of the 16.th century, when classic algebra was emerging and started being applied to practical problems:

``Quien sabe por Algebra, sabe scientificamente.'' Pedro Nunes (1502-1578) in libro de algebra, 1567, fol 270v.

[ Back to the CAMILA Home Page ]

Jose Nuno Oliveira
Fri Mar 21 11:53:20 WET 1997