Please use this identifier to cite or link to this item:
Title: Behavioural reasoning for conditional equations
Author: Martins, Manuel A.
Pigozzi, D.
Keywords: Data structures
Equivalence classes
Specification languages
Behavioural equivalence
Behavioural reasoning
Hidden data
Specification logics
Object oriented programming
Issue Date: 2007
Abstract: Object-oriented (OO) programming techniques can be applied to equational specification logics by distinguishing visible data from hidden data (that is, by distinguishing the output of methods from the objects to which the methods apply), and then focusing on the behavioural equivalence of hidden data in the sense introduced by H. Reichel in 1984. Equational specification logics structured in this way are called hidden equational logics, HELs. The central problem is how to extend the specification of a given HEL to a specification of behavioural equivalence in a computationally effective way. S. Buss and G. Roşu showed in 2000 that this is not possible in general, but much work has been done on the partial specification of behavioural equivalence for a wide class of HELs. The OO connection suggests the use of coalgebraic methods, and J. Goguen and his collaborators have developed coinductive processes that depend on an appropriate choice of a cobasis, which is a special set of contexts that generates a subset of the behavioural equivalence relation. In this paper the theoretical aspects of coinduction are investigated, specifically its role as a supplement to standard equational logic for determining behavioural equivalence. Various forms of coinduction are explored. A simple characterisation is given of those HELs that are behaviourally specifiable. Those sets of conditional equations that constitute a complete, finite cobasis for a HEL are characterised in terms of the HEL's specification. Behavioural equivalence, in the form of logical equivalence, is also an important concept for single-sorted logics, for example, sentential logics such as the classical propositional logic. The paper is an application of the methods developed through the extensive work that has been done in this area on HELs, and to a broader class of logics that encompasses both sentential logics and HELs. © 2007 Cambridge University Press.
Peer review: yes
DOI: 10.1017/S0960129507006305
ISSN: 0960-1295
Appears in Collections:DMat - Artigos

Files in This Item:
File Description SizeFormat 
BRCE.pdfPreprint356.14 kBAdobe PDFView/Open

Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.