Abstract
Observability and reachability are important concepts in formal software development. While observability concepts allow to specify the required observable behavior of a program or system, reachability concepts are used to describe the underlying data in terms of data type constructors. In this paper we show that there is a duality between observability and reachability, both from a methodological and from a formal point of view. In particular, we establish a correspondence between observer operations and data type constructors, observational algebras and constructor-based algebras, and observational and inductive properties of specifications. Our study is based on the observational logic institution [7] and on a novel treatment of reachability which introduces the institution of constructor-based logic. The duality between both concepts is formalised in a category-theoretic setting.
This work is partially supported by the ESPRIT Working Group 29432 CoFI and by the Bayer. Forschungsstiftung.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. Adámek, H. Herrlich, and G. Strecker. Abstract and Concrete Categories. John Wiley & Sons, 1990.
M.A. Arbib and E.G. Manes. Adjoint machines, state-behaviour machines, and duality. Journ. of Pure and Applied Algebra, 6:313–344, 1975.
M. Bidoit and R. Hennicker. Observer complete definitions are behaviourally coherent. In OBJ/CafeOBJ/Maude at Formal Methods’ 99, pages 83–94. THETA, 1999.
M. Bidoit, R. Hennicker, and M. Wirsing. Behavioural and abstractor specifications. Science of Computer Programming, 25:149–186, 1995.
J. Goguen and R. Burstall. Institutions: abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39 (1):95–146, 1992.
J. Goguen and G. Roşu. Hiding more of hidden algebra. In J.M. Wing, J. Woodcock, and J. Davies, editors, Formal Methods (FM’99), volume 1709 of LNCS, pages 1704–1719. Springer, 1999.
R. Hennicker and M. Bidoit. Observational logic. In Armando Haeberer, editor, Algebraic Methodology and Software Technology (AMAST’98), volume 1548 of LNCS. Springer, 1999.
R. Hennicker and A. Kurz. (Ω,Ξ)-logic: On the algebraic extension of coalgebraic specifications. In B. Jacobs and J. Rutten, editors, Coalgebraic Methods in Computer Science (CMCS’99), volume 19 of Electronic Notes in Theoretical Computer Science, pages 195–211, 1999.
C.A.R. Hoare. Proofs of correctness of data representations. Acta Informatica, 1:271–281, 1972.
M. Hofmann and D.T. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. In TAPSOFT’ 95, volume 915 of LNCS, pages 247–261. Springer, 1995.
B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62, 1997.
R. E. Kalman, P. L. Falb, and M. A. Arbib. Topics in Mathematical System Theory. McGraw-Hill, 1969.
J. Loeckx, H.-D. Ehrich, and M. Wolf. Specification of Abstract Data Types. Wiley and Teubner, 1996.
Grant Malcolm. Behavioural equivalence, bisimulation, and minimal realisation. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors, Recent Trends in Data Type Specification, volume 1130 of LNCS, pages 359–378. Springer, 1996.
CoFI Task Group on Language Design. Casl-the cofi algebraic specification language-summary. http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary/.
Horst Reichel. Initial computability, algebraic specifications, and partial algebras. Oxford, Clarendon Press, 1987.
D.T. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal Comput. System Sci., 34:150–178, 1987.
D.T. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165–210, 1988.
M. Wirsing and M. Broy. A modular framework for specification and information. In F. Orejas J. Diaz, editor, TAPSOFT’ 89, volume 351 of LNCS, pages 42–73. Springer, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bidoit, M., Hennicker, R., Kurz, A. (2001). On the Duality between Observability and Reachability. In: Honsell, F., Miculan, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2001. Lecture Notes in Computer Science, vol 2030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45315-6_5
Download citation
DOI: https://doi.org/10.1007/3-540-45315-6_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41864-1
Online ISBN: 978-3-540-45315-4
eBook Packages: Springer Book Archive