> Congress / Final Programme / Tutorials / Tut11
Tut11: Formal reasoning about systems, software and hardware using functionals, predicates and relations
Room: Servanty
Presenter:
Raymond Boute, INTEC- Ghent University, Belgium
Abstract
Formal reasoning in the sense of "letting the symbols do the work" was Leibniz's dream, but making it possible and convenient for everyday practice irrespective of the availability of automated tools is due to the calculational approach that emerged from Computing Science.
This tutorial provides an initiation in a formal calculational approach that covers not only the discrete world of software and digital hardware, but also the "continuous" world of analog systems and circuits. The formalism used is free of the defects of traditional notation that hamper formal calculation, yet, by the unified way in which it captures the conventions from applied mathematics, it is readily adoptable by engineers.
The fundamental part formalizes the equational calculation style found so convenient ever since the first exposure to high school algebra, followed by concepts supporting expression with variables (pointwise) and without (point-free). Calculation rules are derived for (i) proposition calculus, including a few techniques for fast "head" calculation; (ii) sets; (iii) functions, with a basic library of generic functionals that are useful throughout continuous and discrete mathematics; (iv) predicate calculus, making formal calculation with quantifiers as "routine" as derivatives and integrals in engineering mathematics. Pointwise and point-free forms are covered. Uniform principles for designing convenient operators in diverse areas of discourse are presented. Mathematical induction is formalized in a way that avoids the common errors observed in informal use. Illustrative examples are provided throughout.
The applications part shows how to use the formalism in areas of computing, including data type definition, systems specification, imperative and functional programming, formal semantics, deriving theories of programming, and also in other areas such as signal processing (analog and digital), control and telecommunications (formal calculation with Fourier and Laplace transforms) and, as time permits, other topics that may be decided on the spot depending on preferences of the audience.
Presenter
Raymond Boute holds M.Sc. degrees in EE/ME and in Electronics from Ghent University, and a PhD degree in EE from Stanford University. From 1973-1981, he was with Bell Telephone, 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. From 1981-1994, he was a full professor at Nijmegen University, 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. 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, at the Eindhoven University of Technology and, as a Visiting Professor, at the EPFL in Lausanne (1982, 1993), at the ETH in Zuerich (1986), and at the University of Leuven / IMEC (1989).
|
