|Home / Volume 6 / Issue 1 / Paper Abstract: Behavioural Coherence in Object-Oriented Algebraic Specification|
Behavioural Coherence in Object-Oriented Algebraic Specification1
Razvan Diaconescu (Institute of Mathematics of the
Kokichi Futatsugi (Japan Advanced Institute of Science
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
|Articles by Category - Articles by Author - What's New - Submit a Paper|