Externalized and Internalized Notions of Behavioral Refinement

  • Michel Bidoit
  • Rolf Hennicker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


Many different behavioral refinement notions for algebraic specifications have been proposed in the literature but the relationship between the various concepts is still unclear. In this paper we provide a classification and a comparative study of behavioral refinements according to two directions, the externalized approach which uses an explicit behavioral abstraction operator that is applied to the specification to be implemented, and the internalized approach which uses a built-in behavioral semantics of specifications. We show that both concepts are equivalent under suitable conditions. The formal basis of our study is provided by the COL institution (constructor-based observational logic). Hence, as a side-effect of our study on internalized behavioral refinements, we introduce also a novel concept of behavioral refinement for COL-specifications.


Externalize View Reduct Functor Signature Morphism Vertical Composition Implementation Constructor 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.): Algebraic Foundations of Systems Specification. Springer, Heidelberg (1999)Google Scholar
  2. 2.
    Astesiano, E., Kirchner, H., Bidoit, M., Krieg-Brückner, B., Mosses, P.D., Sannella, D.T., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science 286(2), 153–196 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Bidoit, M., Hennicker, R.: Modular correctness proofs of behavioural implementations. Acta Informatica 35, 951–1005 (1998)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Bidoit, M., Hennicker, R.: Constructor-based observational logic. Journal of Logic and Algebraic Programming (2005) (to appear), Preliminary version available at
  6. 6.
    Bidoit, M., Hennicker, R.: Observer complete definitions are behaviourally coherent. In: Proc. OBJ/CafeOBJ/Maude Workshop at Formal Methods 1999, Toulouse, France, September 1999, THETA, pp. 83–94 (1999)Google Scholar
  7. 7.
    Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer Programming 25(2–3), 149–186 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Ehrig, H., Kreowski, H.-J.: Refinement and implementation. In: [1], ch. 7, pp. 201–242. Springer, Heidelberg (1999)Google Scholar
  9. 9.
    Goguen, J., Meseguer, J.A.: Universal realization, persistent interconnection and implementation of abstract modules. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 265–281. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Hennicker, R.: Observational implementation of algebraic specifications. Acta Informatica 35, 951–1005 (1998)CrossRefMathSciNetGoogle Scholar
  13. 13.
    Malcolm, G., Goguen, J.: Proving correctness of refinement and implementation. Technical Report PRG-114, Oxford University Computing Laboratory (1994)Google Scholar
  14. 14.
    Misiak, M.: Behavioural semantics of algebraic specifications in arbitrary logical systems. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 144–161. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  15. 15.
    Nivela, M.P., Orejas, F.: Initial behaviour semantics for algebraic specifications. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol. 332, pp. 184–207. Springer, Heidelberg (1988)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Sannella, D., Tarlecki, A.: On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34, 150–178 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Sannella, D.T., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica 25, 233–281 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Schoett, O.: Data abstraction and correctness of modular programming. Technical Report CST-42-87, University of Edinburgh (1987)Google Scholar
  21. 21.
    Tarlecki, A.: Institutions: An Abstract Framework for Formal Specification. In: [1], ch. 4, pp. 105–130. Springer, Heidelberg (1999)Google Scholar
  22. 22.
    Wirsing, M.: Algebraic Specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 13, pp. 676–788. Elsevier Science Publishers B.V., Amsterdam (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Michel Bidoit
    • 1
  • Rolf Hennicker
    • 2
  1. 1.Laboratoire Spécification et Vérification (LSV), CNRS & ENS de CachanFrance
  2. 2.Institut für InformatikLudwig-Maximilians-Universität MünchenGermany

Personalised recommendations