Behavioural Coherence in Object-Oriented Algebraic Specification¹

Razvan Diaconescu (Institute of Mathematics of the Romanian Academy)
diacon@stoilow.imar.ro

Kokichi Futatsugi (Japan Advanced Institute of Science and Technology)
kokichi@jaist.ac.jp

Abstract: We extend the classical hidden algebra formalism by a re-arrangement of the basic concepts. This re-arrangement of the hidden algebra formalism permits an extension to novel concepts which bring new practical strength to the specification and verification methodologies. The main novel concept, which constitutes the core of this work, is that of behavioural coherence, which is essentially a property of preservation of behavioural structures. We define this concept and study its main denotational and computational properties, and also show how the extension of hidden algebra with behavioural coherence still accommodates the coinduction proof method advocated by classical hidden algebra and, very importantly, permits operations with several hidden sorts in the arity. The emphasis of this paper is however on the methodologies related to behavioural coherence. We present the basic methodologies of behavioural coherence by means of examples actually run under the system, including many proofs with the system exiled to appendices.

Keywords: behavioural equivalence, hidden algebra, behavioural coherence

Category: F.3.2

----------------------
¹C.S.Calude and G.Stefanescu (eds.). Automata, Logic, and Computability. Special issue dedicated to Professor Sergiu Rudeanu Festschrift.