Recent Trends in Data Type Specification

Frontmatter

Towards an algebraic semantics for the object paradigm

Abstract

This paper surveys our current state of knowledge (and ignorance) on the use of hidden sorted algebra as a foundation for the object paradigm. Our main goal is to support equational reasoning about properties of concurrent systems of objects, because of its simple and efficient mechanisation. We show how equational specifications can describe objects, inheritance and modules; our treatment of the latter topic emphasises the importance of reuse, and the rôle of the so-called Satisfaction Condition. We then consider how to prove things about objects, how to unify the object and logic paradigms by using logical variables that range over objects, and how to connect objects into concurrent systems. We provide a universal characterisation of parallel connection, and more generally, of parallel connection with synchronisation, and show how the former construction gives a class manager that provides unique identifiers for its objects. The paper concludes with some topics for further research.

Joseph A. Goguen, Razvan Diaconescu

Rewriting techniques for software engineering

Abstract

This paper surveys the use of rewriting for prototyping languages based on equations as are algebraic specifications. The option is to stress the variety of questions expressed as logical queries that can be solved by using rewriting techniques, without hiding the limitations of the method. Using rewriting itself as a specification language is investigated next. Recent trends in rewriting are briefly sketched.

Jean-Pierre Jouannaud

Identity and existence, and types in algebra

A survey of sorts

Abstract

We survey partiality as found in algebra covering the various approaches which have surfaced and are being used in computer science, particularly in the data type community.

Axel Poigné

Overloading and inheritance

Abstract

This paper reports on some recent investigations aimed at separating and clarifying a number of concepts that frequently appear in object-based and object-oriented languages. Concepts considered include are over-loading, encapsulation, the message paradigm, and a limited form of inheritance. We also introduce formulations of the concepts of overload-systems and coercion-systems, and we present a treatment of (+, ×)-recursive classes and the definition of primitive recursive functions over such classes.

Eric G. Wagner

A SMoLCS based kit for defining high-level algebraic Petri nets

Mohamed Bettaz, Gianna Reggio

Institutions for very abstract specifications

M. Cerioli, G. Reggio

About the “correctness” and “adequacy” of PLUSS specifications

Abstract

In the context of algebraic specifications written in Pluss, this paper investigates various issues raised by the question: “Is my specification correct?”. Up to now the only ways to check the adequacy of a specification with respect to the problem to be solved are through running a prototype on appropriate examples, or through the use of the specification to prove consequent (expected) properties. Before this problem may be fully addressed, issues regarding the specification consistency and the correctness of the prototype w.r.t. the specification must be studied. In this paper, various issues concerning checking consistency and proving properties of PLUSS specifications are presented. It is investigated how general properties can be proved using an appropriate presentation of the specification that may be understood by a prototyping tool. While this study is done in the framework of the pluss specification language, it should be clear that most of the issues considered here arise in a similar way with other specification languages.

Christine Choppy

Semantic constructions in the specification language Glider

S. Clérici, R. Jiménez, F. Orejas

On certification of specifications for TROLL light objects

Abstract

In this paper we informally present a certification calculus for the object specification language TROLL light. The language supports the state- and behavior-oriented specification of information systems. It allows orthogonal construction of large systems from subsystems. The certification calculus provides a basis for verifying properties of specified objects. Besides an introduction to this calculus we show how formulae of this calculus can be derived from TROLL light specifications. The transformation from specification language into calculus shall later be done automatically. Furthermore, we demonstrate proving of object properties by means of an example.

Stefan Conrad

Translating TROLL light concepts to Maude

Abstract

The specification language TROLL light is designed for the conceptual modeling of information systems. Maude is a logic programming language, which unifies the two paradigms of functional and concurrent object-oriented programming. Because of the very similar features offered by both languages, we present a translation from TROLL light concepts into the Maude language in order to compare the languages. Apart from presenting the translation, the languages are briefly described and illustrated by examples.

G. Denker, M. Gogolla

Algebraic high level nets

Petri nets revisited

Abstract

Petri nets, well established as a fundamental model of concurrency and as a specification technique for distributed systems, are revisited from an algebraic point of view. In a first step Petri nets can be considered as monoids with well-defined algebraic semantics. Secondly they can be combined with algebraic specifications leading to the concept of algebraic high-level nets with suitable compositionality results. The main idea of this paper is to present a revised version of algebraic high-level nets (AHL-nets) and to introduce AHL-net-transformation systems. This is a concept of high-level replacement systems for AHL-nets allowing to build up AHL-nets from basic components and to transform them using rules or productions in the sense of graph grammars. This is illustrated by extending the well-known example of “dining philosophers” to a “restaurant of dining philosophers”. Moreover we are able to extend main results from the theory of graph grammars, including local Church-Rosser, parallelism and canonical derivation theorems, to AHL-net-transformation systems. This allows to analyze concurrency in nets not only on the token level but also on the level of transformations of the net structure.

Hartmut Ehrig, Julia Padberg, Leila Ribeiro

2-Categorical specification of partial algebras

Abstract

The purpose of this paper is to present a short survey of possible results of an application of general concepts from categorical algebra to the specification of partial algebras with conditional existence equations. The general concept, which models theories (= formulas and equivalence classes of terms) as categories, is extended to 2-categories, such that rewriting between terms can be made explicit. To make clear the benefits of such an approach the results are presented in the usual terminology of algebraic specifications.

Martin Große-Rhode, Uwe Wolter

A behavioural algebraic framework for modular system design with reuse

Abstract

A formal framework for the design of modular software systems is presented which incorporates the idea of reusing software components in new applications. The approach is based on structured algebraic specifications with behavioural semantics. In order to provide a clean interconnection mechanism for specifications, behavioural specifications with import interfaces are considered and their composition with respect to the behavioural requirements of the import interface is defined. A simple implementation notion for behavioural specifications with import interface is presented which is compatible with the composition of specifications. Hence it is guaranteed that separately developed implementations of parts of an abstract system specification can be automatically composed to a globally correct system implementation. Based on these concepts, reusable components are defined as (unordered) trees of behavioural specifications with import interfaces such that two consecutive nodes are related by the implementation relation. A formal method for the systematic reuse of components in new applications is proposed. The method consists of four steps which describe how to construct for a given abstract system specification a modular implementation by reusing existing implementations available as leaves of appropriate reusable components. The method is demonstrated by a detailed example.

Rolf Hennicker, Friederike Nickl

On fibred adjunctions and completeness for fibred categories

Abstract

We show how the completeness and cocompleteness of the total category of a fibration can be inferred from that of the fibre categories and its base. Our results are somewhat stronger than those in [BGT91] and they are obtained as direct consequences of an important property of general fibred adjunctions. Our aim is to show that fibred category theory can provide insight into constructions of relevance in algebraic specifications, e.g. limits and colimits of many-sorted algebras, by explaining them at a natural level of abstraction.

Claudio Hermida

Implementing inequality and nondeterministic specifications with bi-rewriting systems

Abstract

Rewriting with non-symmetric relations can be considered as a computational model of many specification languages based on non-symmetric relations. For instance, Logics of Inequalities, Ordered Algebras, Rewriting Logic, Order-Sorted Algebras, Subset Logic, Unified Algebras, taxonomies, subtypes, Refinement Calculus, all them use some kind of non-symmetric relation on expressions. We have developed an operational semantics for these inequality specifications named bi-rewriting systems. In this paper we show the applicability of bi-rewriting systems to Unified Algebras and nondeterministic specifications. In the first case, we give a canonical bi-rewriting system implementing the basic theory of these algebras. In the second case, nondeterministic specifications are viewed as inclusion specifications, thus bi-rewriting is a sound, although not always complete deduction method. We show how a specification has to be completed in order to have both soundness and completeness.

Jordi Levy, Jaume Agustí

A semantic basis for logic-independent transformation

Abstract

This paper is based on previous work by Harper, Sannella and Tarlecki who suggest a framework for giving semantic interpretations to logic representations in the LF logical framework. Besides LF, there are also other approaches that tackle the representation of logics in a meta-logic. The logic-independent aspect in the formal development of software has been investigated intensively based on abstract model theory. Less attention is paid to the proof system aspect. In this paper we treat logic-independence by considering the consequence relation that models a proof system for a logic. The existing work is generalized here to the consideration of any logic as a meta-logic, since there may be meta-logics other than LF that are more suitable and convenient for developing “object” logical systems. This generalized framework is then used for building logic-independent specifications and developments. The setting can eventually be considered as a firm semantic basis for developing logic-independent transformations.

Junbo Liu

Unified algebras and abstract syntax

Abstract

We consider the algebraic specification of abstract syntax in the framework of unified algebras. We illustrate the expressiveness of unified algebraic specifications, and provide a grammar-like notation for specifying abstract syntax, particularly attractive for use in semantic descriptions of full-scale programming languages.

Peter D. Mosses

Structured inheritance for algebraic class specifications

Abstract

Inheritance is considered as a binary relation between two classes. Using an algebraic model of class specification, we distinguish between reusing inheritance and specialization inheritance, although the latter is sufficient to simulate the former. We propose mechanisms to derive inherited classes whose behavior can be described in a clean way in terms of the behavior of the superclasses. Among these mechanisms, the instantiation of parameters is seen as a special case of specialization inheritance but not of equal expressive power. A formalization of the intuitive notion of subtyping is then related to the stronger inheritance.

F. Parisi Presicce, A. Pierantonio

Towards a theory for the animation of algebraic specifications

Abstract

Conceptual ideas are developed to provide algebraic specifications with animation, i.e. graphics — possibly moving — of datas and their operations.

We are convinced that animation

• helps to understand algebraic specifications easier
• supports error detection
• supports the operational view
• and improves the acceptance of specifications.

In our theory we emphasize the connection between building the terms of a specification and visualizing this term. To achive this we assign to every constant in the signature of the specification SPEC = (SIG,E) a graphic and to every operation in SIG instructions, how to manipulate the argument graphs. The assignment between terms and graphs is realized as an implementation, especially a graphical implementation by so called basic graphic algebra BaGrA, where all the graphical basic operations like linedrawing etc. and other types, are collected. The graphical implementation is compatible with the actualization of parameterized specifications. An example is given to visualize our ideas of animation.

Catharina Rieckhoff

Second-order proof systems for algebraic specification languages

Abstract

Besides explicit axioms, an algebraic specification language contains model-theoretic constraints such as term-generation or initiality. For proving properties of specifications and refining them to programs, an axiomatization of these constraints is needed; unfortunately, no effective, sound and complete proof system can be constructed for most algebraic specification languages.

In this paper, we construct non-effective second-order axiomatizations for constraints commonly found in specification languages, and simplified forms useful for the universal fragment. They are shown to be sound and complete, but not effective, since the underlying second-order logic is not effective. A good level of machine support is still possible using higher-order proof assistants.

Pierre-Yves Schobbens

An institution of object behaviour

Abstract

An institution for a simple logic of behaviour is built using a cofibration from a category of transition systems into the envisaged category of signatures. The chosen propositional, linear temporal logic distinguishes between event occurrence and event enabling. The satisfaction condition is proved using a fibered adjunction between transition systems and their computations. The operational semantics of behaviour specifications is briefly discussed.

Amílcar Sernadas, José Félix Costa, Cristina Sernadas

Backmatter