Computer-Aided Refinement of Data Structures on Higher-Order Algebraic Specifications

  • Walter Dosch
  • Sönke Magnussen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3026)


The paper studies the transformational refinement of data structures in the framework of higher-order algebraic specifications. We present novel procedures that mechanize the refinement of entire data structures within a single complex transformation step. The transformations validate a general refinement relation that captures different types of simulations. General transformation rules describe algebraic implementations based on abstraction and representation functions. Specialized transformations cover particular changes between data structures. All transformation procedures have been implemented in the Lübeck Transformation System. The system uses analysis algorithms to establish the soundness conditions of the transformations by syntactic criteria. We report practical experiences about manipulating data structures with the system. The paper summarizes results from the second author’s PhD thesis [20].


Higher-order algebraic specification refinement of data structure algebraic implementation transformation system 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Back, R.-J., von Wright, J.: Refinement Calculus, A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  2. 2.
    Bauer, F.L., Möller, B., Partsch, H., Pepper, P.: Formal program construction by transformation computer-aided, intuition-guided programming. IEEE Transactions on Software Engineering 15, 165–180 (1989)zbMATHCrossRefGoogle Scholar
  3. 3.
    Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer Programming 25(2-3), 149–186 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer Programming 25(2-3), 149–186 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Broy, M., Möller, B., Wirsing, M.: Algebraic implementations preserve program correctness. Science of Computer Programming 7, 35–53 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Burstall, R.M., Goguen, J.A.: Putting theories together to make specifications. In: Proc. 5th Intl. Joint Conference on Artificial Intelligence, pp. 1045–1058 (1977)Google Scholar
  7. 7.
    de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998)zbMATHCrossRefGoogle Scholar
  8. 8.
    Dijkstra, E.W.: Notes on structured programming. In: Dahl, O., Dijkstra, E.W., Hoare, C.A.R. (eds.) Structured Programming, Academic Press, London (1971)Google Scholar
  9. 9.
    Dosch, W., Magnussen, S.: Algebraic data structure refinement with the Lübeck Transformation System. In: Indermark, K., Noll, T. (eds.) Kolloquium Programmiersprachen und Grundlagen der Programmierung, number AIB2001-11 in Aachener Informatik Berichte, Rurberg, Oktober 2001, RWTH Aachen, pp. 7–12 (2001)Google Scholar
  10. 10.
    Dosch, W., Magnussen, S.: Computer aided fusion for algebraic program derivation. Nordic Journal of Computing 8(3), 279–297 (2001)zbMATHGoogle Scholar
  11. 11.
    Dosch, W., Magnussen, S.: Lübeck Transformation System: A transformation system for equational higher-order algebraic specifications. In: Cerioli, M., Reggio, G. (eds.) WADT 2001 and CoFI WG Meeting 2001. LNCS, vol. 2267, pp. 85–108. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Ebbinghaus, H.-D., Flum, J., Thomas, W.: Einführung in die mathematische Logik. Spektrum Verlag (1996)Google Scholar
  13. 13.
    Ehrich, H.-D., Gogolla, M., Lippek, U.W.: Algebraische Spezifikation abstrakter Datentypen. Teubner, Stuttgart (1989)zbMATHGoogle Scholar
  14. 14.
    Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specifications 1, Equations and Initial Semantics. EATCS Monographs on Theoretial Computer Science, vol. 6. Springer, Heidelberg (1985)Google Scholar
  15. 15.
    Feather, M.: A survey and classification of some program transformation approaches and techniques. In: Meertens, L.G.L.T. (ed.) Proceedings TC2 Working Conference on Program Specification and Transformation, pp. 165–195. North Holland, Amsterdam (1987)Google Scholar
  16. 16.
    Hearn, B.M., Meinke, K.: ATLAS: A typed language for algebraic specifications. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, pp. 146–168. Springer, Heidelberg (1994)Google Scholar
  17. 17.
    Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)zbMATHCrossRefGoogle Scholar
  18. 18.
    Loeckx, J., Ehrich, H.-D., Wolf, M.: Specification of Abstract Data Types. Wiley&Teubner (1996)Google Scholar
  19. 19.
    Loeckx, J., Ehrich, H.-D., Wolf, M.: Algebraic specification of abstract data types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 5, pp. 217–316. Oxford Science Publications (2000)Google Scholar
  20. 20.
    Magnussen, S.J.: Mechanizing the Transformation of Higher-Order Algebraic Specifications for the Development of Software Systems. Logos Verlag, Berlin (2003)Google Scholar
  21. 21.
    Meinke, K.: Universal algebra in higher types. Theoretical Computer Science 100, 385–417 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Meinke, K., Tucker, J.V.: Universal algebra. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 1, pp. 189–411. Oxford Science Publications (1992)Google Scholar
  23. 23.
    Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 675–788. Elsevier Science Publishers, Amsterdam (1990)Google Scholar
  24. 24.
    Wirsing, M., Partsch, H., Pepper, P., Dosch, W., Broy, M.: On hierarchies of abstract data types. Acta Informatica 20, 1–33 (1983)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Walter Dosch
    • 1
  • Sönke Magnussen
    • 2
  1. 1.Institute of Software Technology and Programming LanguagesUniversity of LübeckLübeckGermany
  2. 2.Lufthansa Revenue ServicesApplication ManagementNorderstedtGermany

Personalised recommendations