Interchange format for inter-operability of tools and translation

The Salsa and Asspegique+/LP Experience
  • Michel Bidoit
  • Christine Choppy
  • Frédéric Voisin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


This paper presents a technical approach for solving the problem of inter-operability between the different existing tools and languages for algebraic specifications. We discuss some semantic compatibility criteria required to ensure a minimal level of inter-operability, we describe a proposal for a specification interchange format, and we explain the mechanisms needed to solve the issues raised by user interaction. The technical generic solutions described in this paper were implemented and experimented in the framework of the Salsa project and when building an interface between Asspegique+ and LP.


Specification Language Logical Framework Proof Assistant Concrete Syntax Interchange Format 
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.
    The Common Framework Initiative. Web home page available at the address, 1995.Google Scholar
  2. 2.
    D. Bert, P. Drabik, and R. Echahed. Manuel de référence de Lpg. Technical Report 17, IMAG-LIFIA, 1987.Google Scholar
  3. 3.
    D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In ESOP-86, pages 119–132. Springer-Verlag L.N.C.S. 213, 1986.Google Scholar
  4. 4.
    M. Bidoit. Pluss, un langage pour le développement de spécifications algébriques modulaires. Thèse d'Etat, Université Paris-Sud, 1989.Google Scholar
  5. 5.
    M. Bidoit, C. Choppy, and F. Voisin. The Asspegique specification environment: Motivations and Design. In Proc. of the 3rd Workshop on Theory and Applications of Abstract Data Types, pages 54–72. Springer-Verlag I.F.B. 116, 1984.Google Scholar
  6. 6.
    M. Bidoit, M.-C. Gaudel, and A. Mauboussin. How to make algebraic specifications more understandable? An experiment with the Pluss specification language. Science of Computer Programming, 12(1), 1989.Google Scholar
  7. 7.
    M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas, and D. Sannella, editors. Algebraic System Specification and Development — A Survey and Annotated Bibliography, volume 501 of Lecture Notes in Computer Science. Springer-Verlag, 1991.Google Scholar
  8. 8.
    R.M. Burstall and J. A. Goguen. The semantics of Clear, a specification language. In Advance Course on Abstract Software Specifications, pages 292–332. Springer-Verlag L.N.C.S. 86, 1980.Google Scholar
  9. 9.
    M. Cerioli. Relationships between Logical Formalisms. PhD Thesis, TD-4-93, Universita di Pisa-Genova-Udine, 1993.Google Scholar
  10. 10.
    C. Choppy. Asspegique: User's Manual. L.R.I. Research Report 452, 1988.Google Scholar
  11. 11.
    C. Choppy. About the “correctness” and “adequacy” of Pluss specifications. In H. Ehrig and F. Orejas, editors, Recent Trends in Data Type Specifications — 9th Workshop on Abstract Data Type joint with 4th COMPASS Workshop — Selected Papers, pages 128–143. L.N.C.S. 785 Springer Verlag, 1994.Google Scholar
  12. 12.
    C. Choppy. Spécifications algébriques: Prototypage et validation. Habilitation à diriger des recherches — Université Paris-Sud, 1994.Google Scholar
  13. 13.
    C. Choppy and M. Bidoit. Integrating Asspegique and LP. In U. Martin and J. Wing, editors, Proceedings of the First International Workshop on Larch, pages 69–85. Springer-Verlag Workshops in Computing, 1993.Google Scholar
  14. 14.
    S. Clérici, R. Jiménez, and F. Orejas. Semantic Constructions in the Specification Language Glider. Technical Report Dissem-033-P, Icarus, June 1992.Google Scholar
  15. 15.
    H. Ehrig, W. Fey, and H. Hansen. Act One: an algebraic specification language with two levels of semantics. Technical Report 83-03, TU Berlin FB 20, 1983.Google Scholar
  16. 16.
    R. Forgaard and J. Guttag. Reve: a term rewriting system generator with failure-resistant Knuth-Bendix, 1984. Proc. of an NSF workshop on the rewrite rule laboratory, and Report n∘ 84GEN008, General Electric.Google Scholar
  17. 17.
    S. Garland and J. Guttag. An overview of LP, the Larch Prover. In Proc. of the Third International Conference on Rewriting Techniques and Applications, pages 137–151. Springer-Verlag L.N.C.S. 355, 1989.Google Scholar
  18. 18.
    S. Garland and J. Guttag. A Guide to LP, The Larch Prover. Technical Report 82, DEC-SRC, 1991.Google Scholar
  19. 19.
    M.-C. Gaudel. Structuring and modularizing algebraic specifications: the Pluss specification language, evolutions and perspectives. In Proc. of the 9th Symposium on Theoretical Aspects of Computer Science (STACS), pages 3–23. Springer-Verlag L.N.C.S. 577, 1992.Google Scholar
  20. 20.
    J. A. Goguen and R.M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39:95–146, 1992.Google Scholar
  21. 21.
    Salsa (group composed of D. Bert, M. Bidoit, C. Choppy, R. Echahed, J.-M. Hufflein, J.-P. Jacquot, M. Lemoine, N. Levy, J.-C. Reynaud, C. Roques, and F. Voisin). Opération Salsa: Structure d'AccueiL pour Spécifications Algébriques. Final report, December 1993.Google Scholar
  22. 22.
    S. Kaplan and C. Choppy. Abstract rewriting with concrete operators. In Proc. of the Third International Conference on Rewriting Techniques and Applications, pages 178–186. Springer-Verlag L.N.C.S. 355, 1989.Google Scholar
  23. 23.
    P. Lescanne. Computer experiments with the Reve term rewriting system generator. In Proc. 10th Symposium on Principles of Programming Languages, pages 99–108. ACM, 1983.Google Scholar
  24. 24.
    T. Mossakowski. A hierarchy of institutions separated by properties of parameterized abstract data types. In E. Astesiano, G. Reggio, and A. Tarlecki, editors, Recent Trends in Data Type Specifications — 10th Workshop on Abstract Data Type joint with 5th COMPASS Workshop — Selected Papers, pages 389–405. L.N.C.S. 906 Springer Verlag, 1995.Google Scholar
  25. 25.
    C. Roques. Modularité dans les spécifications algébriques, Théorie et application. Thèse de Doctorat, Université Paris-Sud, 1994.Google Scholar
  26. 26.
    D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165–210, 1988.Google Scholar
  27. 27.
    F. Voisin and M. Bidoit. Towards Modular Theorem-Provers for Modular Algebraic Specifications: Modular Orientation of Equations into Rewrite Rules. Submitted to the proceedings of the 11th WADT, 1995.Google Scholar
  28. 28.
    M. Wirsing. Structured algebraic specifications: A kernel language. Theoretical Computer Science, 42(2):124–249, 1986.Google Scholar
  29. 29.
    M. Wirsing. Algebraic specification languages: an overview. In E. Astesiano, G. Reggio, and A. Tarlecki, editors, Recent Trends in Data Type Specifications10th Workshop on Abstract Data Type joint with 5th COMPASS Workshop — Selected Papers, pages 81–115. L.N.C.S. 906 Springer Verlag, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Michel Bidoit
    • 1
  • Christine Choppy
    • 2
    • 3
  • Frédéric Voisin
    • 3
  1. 1.LIENS, C.N.R.S. U.R.A. 1327 & Ecole Normale SupérieureParis Cedex 05France
  2. 2.IRINUniversité de Nantes & Ecole CentraleNantes Cedex 03France
  3. 3.LRI, C.N.R.S. U.R.A. 410 & Université de Paris-SudOrsay CedexFrance

Personalised recommendations