Skip Navigation

Journal of Logic and Computation 1995 5(5):603-630; doi:10.1093/logcom/5.5.603
© 1995 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by SERNADAS, A.
Right arrow Articles by COSTA, J.{a. F{a.}E.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Articles

Object Specification Logic

AMÍLCAR SERNADAS1, CRISTINA SERNADAS1 and JOSE{acute} F{acute}ELIX COSTA2

1IST, Department of Mathematics Lisbon, Portugal E-mail: acscss{at}raf.ist.utl.pt
2Faculdade de Ciências, Department of Informatics Lisbon, Portugal E-mail: fgc{at}di.fc.up.pt

A logic for specifying and reasoning about object classes and their instances (aspects) is presented and illustrated. This logic is an extension of a rather standard linear temporal, many-sorted, first-order predicate logic with equality. The extensions were designed to be as simple as possible while supporting the envisaged locality of arguments, object specialization and object aggregation. Objects are specified through their aspects. Each aspect establishes a local vocabulary (signature). The logic works at two levels: first, we can specify and prove assertions about a given object aspect in isolation (local reasoning), e.g. persons, patients or cars; second, we can specify interaction constraints and make inferences between aspects within the same community of objects (global reasoning), e.g. carry the theorems of persons onto patients (specialization inheritance) or carry the theorems of persons onto the aggregations of persons and cars (incorporation inheritance). Some reflection mechanisms are also shown to be sound: for instance what becomes true of persons because of the interactions between persons and cars. The proposed logic is given in an axiomatic style.

Keywords: System specification and verification; object-orientation; logic of inheritance; logic of interaction; temporal logic; many-sorted logic


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.