Making CS and classical EE meet: unification by formalization

Raymond T. Boute
INTEC, Ghent University, Belgium

As David Parnas observes, professional engineers are often distinguished from other designers by their ability to use mathematical models. In actual practice, this situation is evident in classical engineering (say, EE), where mathematical models are used routinely, but far from common in applied Computer Science (say, Software Engineering), where "methodologies" with ambitious acronyms but disappointing content prevail.

Part of this is due to differences in educational background but, as argued here, the deeper cause resides in a mathematical style breach: in everyday practice, differential and integral calculus are used in an essentially formal way, but the logical justification of the calculation rules is typically in words, using logic symbols (e.g., quantifiers) only informally as shorthands (called "syncopation" by Paul Taylor). The latter also holds in most areas of Computer Science: formal logic usually remains isolated from, and has little impact on, other areas. However, the calculational style can make formal logic practical for everyday use and a considerable help to intuition in exploring new domains.

This presentation shows how this potential is fully realized by a simple formalism. Its language consists of four constructs only and synthesizes common and new mathematical notations in a problem-free way. It package of rules has two main fundamental components: generic functionals providing rules for calculating with functions in arbitrary domains of discourse, and a functional predicate calculus, allowing engineers to calculate with predicates and quantifiers as smoothly as they have learned to do with derivatives and integrals.

This is illustrated in three stages. (a) Showing the common origin of both components in deriving dataflow realizations from recursive specifications, with applications in the instrumentation and control language LabVIEW. (b) An example of generic functional design, extending the well-known notion of "tolerance" on physical components to mathematical functions. We show simple but interesting particularizations in areas ranging from analog filters in electronics to dependent types and data bases in computing. (c) An example of using functional predicate calculus for describing the dynamics of computer programs by means of program equations and calculationally deriving ante- and postcondition semantics. The resulting predicate transformers formally resemble the use of Green's functions and Fourier transforms in engineering. Due to the conceptual simplicity gained, each of these elaborations is sufficiently brief and simple to take only a few minutes to explain.

Together with references to other results, this provides sufficient evidence that the formalization as presented has the potential of unifying the mathematical style and methodology of Computer Science and classical Engineering disciplines.

Supporting Materials: The slides can be downloaded in pdf format. In additon, Raymound Bout has provided the following [slightly edited -dra]: As promised to Martin Morf, I have provided a more elaborate answer to his question about sum calculation. It has been added to the site as a "service after delivery" to the students as well. In the same spirit, any EE380 student who is interested in exploring the advantages of formal calculation and reasoning in his own area of interest and has in mind a piece of mathematical calculation or reasoning that is currently not as smooth or clear as desired is invited to submit it to me. Subsequently I will see whether it can be polished to make it into a nice example for the approach. The idea is that students may find examples from their own immediate field of interest more appropriate and convincing than examples chosen in advance by the lecturer.

About the speaker:

Raymond Boute holds M.Sc. degrees in EE/ME (1966) and in Electronics (1968) from Ghent University, and a M.Sc. (1969) and a Ph.D. degree (1973) in EE from Stanford University. His thesis supervisor was Prof. Edward McCluskey.

From 1973-1981, he was with Bell Telephone (now Alcatel), Antwerp, working on advanced system concepts, control structures and software for telecommunications systems, and participated in the Intel VLSI processor project on language design for systems programming (1978, 1979).

From 1981-1994, he was a full professor at Nijmegen University (The Netherlands), teaching computer architecture, operating systems, VLSI design, computer networks and satellite communications, and initiating the research and education at Nijmegen on functional programming and more declarative formalisms, especially for hybrid systems.

Since 1994, he continues these research interests as a full professor at Ghent University (Belgium). Teaching includes mathematical foundations for computer science, formal methods in systems modelling, and formal semantics.

He has also taught courses at the University of Antwerp (1976), at the Eindhoven University of Technology (1985-86) and, as a Visiting Professor, at the EPFL in Lausanne (1982, 1993), at the ETH in Zürich (1986), and at the University of Leuven / IMEC (1989).

Contact information:

Raymond T. Boute
INTEC - Universiteit Gent
Sint-Pietersnieuwstraat 41
B-9000 Gent (Belgium)
+32 9 264 3449
+32 9 264 3593
boute@intec.UGent.be