Abstract
We present an institution of observational logic suited for state-based systems specifications. The institution is based on the notion of an observational signature (which incorporates the declaration of a distinguished set of observers) and on observational algebras whose operations are required to be compatible with the indistinguishability relation determined by the given observers. In particular, we introduce a homomorphism concept for observational algebras which adequately expresses observational relationships between algebras. Then we consider a flexible notion of observational signature morphism which guarantees the satisfaction condition of institutions w.r.t. observational satisfaction of arbitrary first-order sentences. From the proof theoretical point of view we construct a sound and complete proof system for the observational consequence relation. Then we consider structured observational specifications and we provide a sound and complete proof system for such specifications by using a general, institution-independent result of [6].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
G. Bernot, M. Bidoit: Proving the correctness of algebraically specified software: modularity and observability issues. Proc. AMAST’ 91, 216–242, Springer-Verlag Works. in Comp. Series, 1992.
M. Bidoit, R. Hennicker: Proving the correctness of behavioural implementations. In Proc. AMAST’ 95, LNCS 936, 152–168, 1995. An extended version entitled “Modular correctness proofs of behavioural implementations” will appear in Acta Informatica.
M. Bidoit, R. Hennicker: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science 175, 3–55, 1996.
M. Bidoit, R. Hennicker, M. Wirsing: Behavioural and abstractor specifications. Science of Computer Programming 25, 149–186, 1995.
M. Bidoit, A. Tarlecki: Behavioural satisfaction and equivalence in concrete model categories. Proc. CAAP’ 96, Trees in Algebra and Progr., LNCS 1059, 241–256, 1996.
T. Borzyszkowski: Completeness of a logical system for structured specifications. In:F. Parisi Presicce (ed.): Recent Trends in Algebraic Development Techniques, LNCS 1376, 107–121, 1998.
R. Burstall, R. Diaconescu: Hiding and behaviour: an institutional approach. In: A. W. Roscoe (ed.): A Classical Mind: Essays in Honour of C.A.R. Hoare, 75–92, Prentice-Hall, 1994.
R. Diaconescu: Behavioural coherence in object-oriented algebraic specification. Japan Advanced Institute for Science and Technology, IS-RR-98-0017F, 1998.
R. Diaconescu, K. Futatsugi: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing, Vol. 6, World Scientific, 1998.
J. Goguen, R. Burstall: Institutions: abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146, 1992.
J. Goguen, G. Malcolm: A hidden agenda. Report CS97-538, Univ. of Calif. at San Diego, 1997.
J. Guttag, J. Horning: Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science, Springer, 1993.
R. Hennicker: Structured specifications with behavioural operators: semantics, proof methods and applications. Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 1997.
R. Hennicker, M. Bidoit: Observational logic (long version). http://www.lsv.enscachan.fr/Publis/RAPPORTS_LSV/, 1998.
R. Hennicker, F. Nickl: A behavioural algebraic framework for modular system design with reuse. In: H. Ehrig, F. Orejas (eds.): Recent Trends in Data Type Specification, LNCS 785, 220–234, 1994.
B. Jacobs, J. Rutten: A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62, 222–259, 1997.
H. J. Keisler: Model theory for infinitary logic. North-Holland, 1971.
J. Loeckx, H.-D. Ehrich, M. Wolf: Specification of Abstract Data Types. Wiley and Teubner, 1996.
G. Malcolm, J. A. Goguen: Proving correctness of refinement and implementation. Technical Monograph PRG-114, Oxford University Computing Laboratory, 1994.
P. Nivela, F. Orejas: Initial behaviour semantics for algebraic specifications. In: D. T. Sannella, A. Tarlecki (eds.): Recent Trends in Data Type Specification, Springer Lecture Notes in Computer Science 332, 184–207, 1988.
P. Padawitz: Swinging data types: syntax, semantics, and theory. In: M. Haveraaen, O. Owe, O.-J. Dahl (eds.): Recent Trends in Data Type Specification, LNCS 1130, 409–435, 1996.
H. Reichel: Initial computability, algebraic specifications, and partial algebras. International Series of Monographs in Computer Science No. 2, Oxford: Clarendon Press, 1987.
H. Reichel: An approach to object semantics based on terminal co-algebras. Math. Struct. Comp. Sci., 5, 129–152, 1995.
D. T. Sannella, A. Tarlecki: Specifications in an arbitrary institution. Information and Computation 76, 165–210, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hennicker, R., Bidoit, M. (1998). Observational Logic. In: Haeberer, A.M. (eds) Algebraic Methodology and Software Technology. AMAST 1999. Lecture Notes in Computer Science, vol 1548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49253-4_20
Download citation
DOI: https://doi.org/10.1007/3-540-49253-4_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65462-9
Online ISBN: 978-3-540-49253-5
eBook Packages: Springer Book Archive