Rodney Martineau Burstall -Rod, as he was known to us all -died on Thursday, 13th February, 2025, after a long illness.Rod was a kind and generous man who will be remembered by those who knew him as much for his humanity as for his contributions to computer science.While he made major contributions to our subject, he constantly demonstrated humility, curiosity, openness, tolerance, and acceptance.He read widely and enjoyed discussing -or learning about -basically any topic that his conversational partner felt passionate about.Perhaps more than anything he exemplified a comfortable way of being human.To many of us that was his greatest contribution to our lives.Rod was born in 1934, the son of a draftsman and a housewife from Liverpool.He attended King George V Grammar School at Southport, moved on to King's College, Cambridge, reading Natural Sciences, and then took a Masters in

This is the second part of a two-part special issue dedicated to the memory of our friend and colleague, Martin Hofmann.The first part was published as Mathematical Structures in Computer Science (2021), 31(9).On 21 January 2018, Martin Hofmann died in a tragic mountain hiking accident in Japan.He was there to attend a workshop at NII Shonan and arrived early for the workshop in order to spend a day climbing Mount Nikkō-Shirane.On his way down from the 2578 m summit, he was caught in a severe snowstorm and lost his way back to safety.

This is the first part of a two-part special issue of Mathematical Structures in Computer Science dedicated to the memory of our friend and colleague, Martin Hofmann.On 21 January 2018, Martin Hofmann died in a tragic mountain hiking accident in Japan.He was there to attend a workshop at NII Shonan and arrived early for the workshop in order to spend a day climbing Mount Nikkō-Shirane.On his way down from the 2578-m summit, he was caught in a severe snowstorm and lost his way back to safety.

We consider structured specifications built from flat specifications using union, translation and hiding with their standard model-class semantics in the context of an arbitrary institution. We examine the alternative of sound property-oriented semantics for such specifications, and study their relationship to model-class semantics. An exact correspondence between the two (completeness) is not achievable in general. We show through general results on property-oriented semantics that the semantics arising from the standard proof system is the strongest sound and compositional property-oriented semantics in a wide class of such semantics. We also sharpen one of the conditions that does guarantee completeness and show that it is a necessary condition.

We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduces some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

Abstract. One of the most novel features of C ASL , the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of C ASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by some details of the features provided in C ASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.

Formal Aspects of Computing are dedicated to Professor Rod Burstall, and, as a collection of papers, memoirs and incidental pieces, form a Festschrift for Rod. The contributions are made by some of the many who know Rod and have been in uenced by him. The research papers included here represent some of the areas in which Rod has been active, and the editors thank their colleagues for agreeing to contribute to this Festschrift.

Abstract The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way. An attempt is made to offer an overall view, rather than new results, and to focus on the basic motivation behind the technicalities presented elsewhere.

An important tool for controlling search in an object logic is the use of structured theory presentations. In order to apply these ideas to the setting of a logical framework, the authors study the behavior of structured theory presentations under representation in a framework, focusing on the problem of lifting presentations, from the object logic to the metalogic of the framework. The authors also consider imposing structure on logic presentations so that logical systems may themselves be defined in a modular fashion. This opens the way to a CLEAR-like language for defining both theories and logics in a logical framework.>

An attempt is made to apply ideas about algebraic specification in the context of a programming language. Standard ML with modules is extended by allowing axioms in module interface specifications and in place of code. The resulting specification language, called Extended ML, is given a semantics based on the primitive specification-building operations of the kernel algebraic specification language ASL. Extended ML provides a framework for the formal development of programs from specifications by stepwise refinement, which is illustrated by means of a simple example. From its semantic basis Extended ML inherits complete independence from the logical system (institution) used to write specifications. This allows different styles of specification as well as different programming languages to be accommodated.

Contrary to popular belief, equational logic with induction is not complete for initial models of equational specifications. Indeed, under some regimes (the Clear specification language and most other algebraic specification languages) no proof system exists which is complete even with respect to ground equations. A collection of known results is presented along with some new observations.