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
This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper's main contribution is to provide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them.

Abstract
The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of p -institutions. This leads to a smooth generalization of the "refinement by interpretation" approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to build up a refinement calculus of structured specifications in and across arbitrary f-institutions. © C.J. Rodrigues, M.A. Martins, A. Madeira & L.S. Barbosa This work is licensed under the Creative Commons Attribution License.

Abstract
Orchestrating software components, often from independent suppliers, became a central concern in software construction. Actually, as relevant as components themselves, are the ways in which they can be put together to interact and cooperate in order to achieve some common goal. Such is the role of the so-called software connectors: external coordination devices which ensure the flow of data and enforce synchronization constraints within a component's network. This paper introduces a new model for software connectors, based on relations extended in time, which aims to provide support for light inter-component dependency and effective external control.

Abstract
Statecharts was conceived as a visual formalism for the design of reactive systems. UML statecharts is an object-based variant of classical statecharts, incorporating several concepts different from the classical statecharts. This paper discusses a coalgebraic description of UML statecharts, directly derived from its operational semantics. In particular such an approach induces suitable notions of equivalence and (behavioral) refinement for statecharts. Finally, a few refinement laws are investigated to support verifiable stepwise system development with statecharts.

Abstract
Argumentation and proof are two main ingredients in strategies for developing mathematical skills and structured reasoning. This paper reports on a research project aimed at 'refactoring' school Mathematics in other to achieve a higher degree of mathematical literacy. In a sense this builds on a number of 'lessons' learnt from the practice of Computing Science. We further argue that mathematical fluency, broadly understood as the ability to reason in terms of abstract models and the effective use of logical arguments and mathematical calculation, became a condition for democratic citizenship and sustainable development. © Springer-Verlag Berlin Heidelberg 2014.