Abstract
This paper presents a survey of formal methods courses in European higher education carried out by the FME Subgroup on Education over the last two years. The survey data sample is made of 117 courses spreading over 58 higher-education institutions across 13 European countries and involving (at least) 91 academic staff. A total number of 364 websites have been browsed which are accessible from the electronic (HTML) version of the paper in the form of links to course websites, lecturers and topic entries in encyclopedias or virtual libraries. Three main projections of our sample are briefly analysed. Although far from being fully representative, these already provide some useful indicators about the impact of formal methods in European curricula on computing. © Springer-Verlag 2004.

Abstract
This paper accompanies the demonstration of CAMILA, an experimental platform for formal software development, rooted in the tradition of constructive specification methods. The CAMILA approach is an attempt to make available at software development level the basic problem solving strategy one got used to from school physics -- create, experiment and reason on a mathematical model. Based on a notion of formal software component, it encompasses a set-theoretic language and an in equational calculus for classification and refinement. Its kernel is a functional prototyping environment, fully connectable to external applications, equipped with a classified component repository and distribution facilities. © Springer-Verlag Berlin Heidelberg 1997.

Abstract

Abstract

Abstract
Theoretical computer science has the aim of formalizing previous empirical, innovative creations in computing, by developing formal methods and models for their description, analysis and design. Formal methods emerged in software engineering as the mathematical support needed for software systems description, design and verification, offering abstract formalisms and domains of models. Interactive software systems design, due to the principle of separation, has been split into two distinct design and implementation processes, one concerned with the computational subsystem, the other addressing the interactive one. However, formal methods have been applied, almost exclusively, in the design of the computational layer. The design of the interactive layer is mainly concerned with the design of the User Interface (UI) of the system or application. Despite its recognized importance and complexity, UI design is still being done on a technological basis and using ad hoc methods. Therefore, it is time to devolve upon user-interface software design the acknowledged benefits derived from the use of formal methods. In this paper, we start by formalizing mechanisms to be embedded in an UI model, appropriate to cope with some characteristics of user input-behaviour, namely, nondeterminism, unreliably and incompleteness. Archetypes are presented as mechanisms for the representation and treatment of incomplete user's input, an innovative step in UI design. We call assisted-user-interfaces (AUI) the class of UI based on such mechanisms. A user-interface development system for their automatic generation, ASSIST, is also described. Finally, we outline an important methodological link between the design of the two layers of an interactive system (interactive and computational). A formal specification of the application contains information that may be systematically used in the design of the relevant parts of the interactive layer. Through ASSIST that information allows for the automatic generation of the AUI. © 1990.

Abstract
Problem statements often resort to superlatives such as in eg. "...the smallest such number", "...the best approximation", "...the longest such list" which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part). This paper introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution being sought. The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with. © 2011 Springer-Verlag.