Abstract
The COL institution (constructor-based observational logic) has been introduced as a formal framework to specify both generation- and observation-oriented properties of software systems. In this paper we consider behavioral refinement relations between COL-specifications taking into account implementation constructions. We propose a general strategy for proving the correctness of such refinements by reduction to (standard) first-order theorem proving with induction. Technically our strategy relies on appropriate proof rules and on a lifting construction to encode the reachability and observability notions of the COL institution.
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.
This work is partially supported by the GLOWA-Danube project (01LW0303A) sponsored by the German Federal Ministry of Education and Research.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.): Algebraic Foundations of Systems Specification. Springer, Heidelberg (1999)
Bidoit, M., Cengarle, M.-V., Hennicker, R.: Proof systems for structured specifications and their refinements. In: [1], ch. 11, pp. 385–433. Springer, Heidelberg (1999)
Bidoit, M., Hennicker, R.: Modular correctness proofs of behavioural implementations. Acta Informatica 35, 951–1005 (1998)
Bidoit, M., Hennicker, R.: Constructor-based observational logic. Journal of Logic and Algebraic Programming 67(1-2), 3–51 (2006), Preliminary version, available at http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf
Bidoit, M., Hennicker, R.: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science 165(1), 3–55 (1996)
Bidoit, M., Hennicker, R.: Observer complete definitions are behaviourally coherent. In: Proc. OBJ/CafeOBJ/Maude Workshop at Formal Methods, Toulouse, France, Septmeber, pp. 83–94. THETA (1999)
Bidoit, M., Hennicker, R.: Externalized and internalized notions of behavioral refinement. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 334–350. Springer, Heidelberg (2005)
Bidoit, M., Mosses, P.D.: CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)
Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing. World Scientific, Singapore (1998)
Ehrig, H., Kreowski, H.-J.: Refinement and implementation. In: [1]. ch:7, pp. 201–242. Springer, Heidelberg (1999)
Goguen, J., Meseguer, J.A.: Universal realization, persistent interconnection and implementation of abstract modules. In: Proc. ICALP 1982. LNCS, vol. 140, pp. 265–281. Springer, Heidelberg (1982)
Goguen, J., Roşu, G.: Hiding more of hidden algebra. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1704–1719. Springer, Heidelberg (1999)
Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)
Loeckx, J., Ehrich, H.-D., Wolf, M.: Specification of Abstract Data Types. Wiley and Teubner (1996)
Malcolm, G., Goguen, J.: Proving correctness of refinement and implementation. Technical Report PRG-114, Oxford University Computing Laboratory (1994)
Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)
Orejas, F., Navarro, M., Sanchez, A.: Implementation and behavioural equivalence. In: Bidoit, M., Choppy, C. (eds.) Abstract Data Types 1991 and COMPASS 1991. LNCS, vol. 655, pp. 93–125. Springer, Heidelberg (1993)
Sannella, D., Tarlecki, A.: On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34, 150–178 (1987)
Sannella, D.T., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica 25, 233–281 (1988)
Schoett, O.: Data abstraction and correctness of modular programming. Technical Report CST-42-87, University of Edinburgh (1987)
Tarlecki, A.: Institutions: An Abstract Framework for Formal Specification. In: [1], ch. 4, pp. 105–130. Springer, Heidelberg (1999)
Wirsing, M.: Algebraic Specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 3, pp. 676–788. Elsevier Science Publishers B.V, Amsterdam (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bidoit, M., Hennicker, R. (2006). Proving Behavioral Refinements of COL-specifications. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_18
Download citation
DOI: https://doi.org/10.1007/11780274_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35462-8
Online ISBN: 978-3-540-35464-2
eBook Packages: Computer ScienceComputer Science (R0)