Abstract
Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In particular it allows for reasoning about confinement in object-oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally.

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
Genericity is a topic which is not sufficiently developed in state-based systems modelling, mainly due to a myriad of approaches and behaviour models which lack unification. This paper adopts coalgebra theory to propose a generic notion of a state-based software component, and an associated calculus, by quantifying over behavioural models specified as strong monads. This leads to the pointfree, calculational reasoning style which is typical of the so-called Bird-Meertens school. ©2003 Published by Elsevier Science B. V.

Abstract
A partial component is a process which fails or dies at some stage, thus exhibiting a finite, more ephemeral behaviour than expected. Partiality-which is the rule rather than exception in formal modelling-can be treated mathematically via totalization techniques. In the case of partial functions, totalization involves error values and exceptions. In the context of a coalgebraic approach to component semantics, this paper argues that the behavioural counterpart to such functional techniques should extend behaviour with try-again cycles preventing from component collapse, thus extending totalization or transposition from the algebraic to the coalgebraic context. We show that a refinement relationship holds between original and totalized components which is reasoned about in a coalgebraic approach to component refinement expressed in the pointfree binary relation calculus. As part of the pragmatic aims of this research, we also address the factorization of every such totalized coalgebra into two coalgebraic components-the original one and an added front-end-which cooperate in a client-server style.

Abstract
A transition system can be presented either as a binary relation or as a coalgebra for the powerset functor, each representation being obtained from the other by transposition. More generally, a coalgebra for a functor F generalises transition systems in the sense that a shape for transitions is determined by F, typically encoding a signature of methods and observers. This paper explores such a duality to frame in purely relational terms coalgebraic refinement, showing that relational (data) refinement of transition relations, in its two variants, downward and upward (functional) simulations, is equivalent to coalgebraic refinement based on backward and forward morphisms, respectively. Going deeper, it is also shown that downward simulation provides a complete relational rule to prove coalgebraic refinement. With such a single rule the paper defines a pre-ordered calculus for refinement of coalgebras, with bisimilarity as the induced equivalence. The calculus is monotonic with respect to the main relational operators and arbitrary relator F, therefore providing a framework for structural reasoning about refinement.