Abstract

Abstract
MathIS is a new project that aims to reinvigorate secondary-school mathematics by exploiting insights of the dynamics of algorithmic problem solving. This paper describes the main ideas that underpin the project. In summary, we propose a central role for formal logic, the development of a calculational style of reasoning, the emphasis on the algorithmic nature of mathematics, and the promotion of self-discovery by the students. These ideas are discussed and the case is made, through a number of examples that show the teaching style that we want to introduce, for their relevance in shaping mathematics training for the years to come. In our opinion, the education of software engineers that work effectively with formal methods and mathematical abstractions should start before university and would benefit from the ideas discussed here.

Abstract

Abstract
Refinement by interpretation replaces signature morphisms by logic interpretations as a means to translate specifications and witness refinements. The approach was recently introduced by the authors [M. A. Martins, A. Madeira, and L. S. Barbosa. Refinement via interpretation. In Proc. of 7th IEEE Int. Conf. on Software Engineering and Formal Methods, Hanoi, Vietnam, November 2009. IEEE Computer Society Press] in the context of equational specifications, in order to capture a number of relevant transformations in software design, reuse and adaptation. This paper goes a step forward and discusses the generalization of this idea to deductive systems of arbitrary dimension. This makes possible, for example, to refine sentential into equational specifications and the latter into modal ones. Moreover, the restriction to logics with finitary consequence relations is dropped which results in increased flexibility along the software development process.

Abstract
Traditional notions of refinement of algebraic specifications, based on signature morphisms, art often too rigid to capture a number of relevant transformations in the context of software design, reuse and adaptation. This paper proposes an alternative notion of specification refinement, building on recent work on logic interpretation. The concept is discussed, its theory partially developed, its use illustrated through a number of examples.

Abstract
Although increasingly popular, Model Driven Architecture (MDA) still lacks suitable formal foundations on top of which rigorous methodologies for the description, analysis and transformation of models could be built. This paper aims to contribute in this direction: building on previous work by the authors on coalgebraic refinement for software components and architectures, it discusses refactoring of models within a coalgebraic semantic framework. Architectures are defined through aggregation based on a coalgebraic semantics for (subsets of) UML. On the other hand, such aggregations, no matter how large and complex they are, can always be dealt with as coalgebras themselves. This paves the way to a discipline of models, transformations which, being invariant under either behavioural equivalence or refinement, are able to formally capture a large number of refactoring patterns. The main ideas underlying this research are presented through a detailed example in the context of refactoring of UML class diagrams.