Advertisement

Integrating HOL-CASL into the Development Graph Manager MAYA

  • Serge Autexier
  • Till Mossakowski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2309)

Abstract

For the recently developed specification language CASL, there exist two different kinds of proof support: While HOL-CASL has its strength in proofs about specifications in-the-small, Maya has been designed for management of proofs in (CASL) specifications in-the-large, within an evolutionary formal software development process involving changes of specifications. In this work, we discuss our integration of HOL-CASL and Maya into a powerful system providing tool support for CASL, which will also serve as a basis for the integration of further proof tools.

Keywords

Source Node Theorem Prover Target Node Proof Obligation Proof Tree 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    S. Autexier, D. Hutter, H. Mantel, and A. Schairer. Towards an evolutionary formal software-development using CASL. In C. Choppy, D. Bert, and P. Mosses, (Eds.), WADT’99, LNAI 1827, 73–88, Springer-Verlag, 2000.Google Scholar
  2. 2.
    R. Boulton, K. Slind, A. Bundy, and M. Gordon: An Interface between CLAM and HOL, In J. Grundy and M. Newey (eds.), Proceedings of TPHOLs’98, LNAI 1479, 87–104, Springer, Canberra, Australia, September/October 1998.Google Scholar
  3. 3.
    M. Cerioli and J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173:311–347, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    CoFI Language Design Task Group. The Common Algebraic Specification Language ( Casl) — Summary, Version 1.0 and additional Note S-9 on Semantics, available from http://www.cofi.info, 1998.
  5. 5.
    L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The PROSPER toolkit. In S. Graf and M. Schwartbach, eds., Tools and Algorithms for Constructing Systems, TACAS, Berlin, Germany, LNAI 1785, 78–92. Springer-Verlag, 2000.Google Scholar
  6. 6.
    R. Diaconescu, J. Goguen, P. Stefaneas. Logical support for modularization, In G. Huet, G. Plotkin, (Eds), Logical Environments, 83–130, Cambridge Press 1991.Google Scholar
  7. 7.
    A. Franke, M. Kohlhase: System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving, In H. Ganzinger (Ed.) Proceedings of the 16 th conference on automated deduction (CADE-16), Trento, Italy. LNAI 1632, 217–221, Springer 1999.Google Scholar
  8. 8.
    D. Hutter: Management of change in structured verification, In Proceedings Automated Software Engineering (ASE-2000), IEEE, 2000.Google Scholar
  9. 9.
    D. Hutter et. al. Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 523–530, 1996.Google Scholar
  10. 10.
    M. Kohlhase: OMDoc: Towards an OPENMATH Representation of Mathematical Documents, SEKI-Report SR-00-02, FR Informatik, Saarland University, 2000, http://www.mathweb.org/omdoc.
  11. 11.
    C. Lüth, H. Tej, Kolyang, and B. Krieg-Brückner. TAS and IsaWin: Tools for transformational program development and theorem proving. In J.-P. Finance, ed., Fundamental Approaches to Software Engineering FASE’99. Joint European Conferences on Theory and Practice of Software ETAPS’99, LNAI 1577, 239–243. Springer Verlag, 1999.Google Scholar
  12. 12.
    C. Lüth and B. Wol.. Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming, 9(2):167–189, March. 1999.zbMATHCrossRefGoogle Scholar
  13. 13.
    T. Mossakowski, S. Autexier, and D. Hutter: Extending Development Graphs With Hiding. In H. Hußmann (Ed.), Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), Genova, Italy. LNAI 2029, 269–283. Springer, 2001.Google Scholar
  14. 14.
    T. Mossakowski, Kolyang, and B. Krieg-Brückner. Static semantic analysis and theorem proving for CASL. In F. Parisi Presicce, ed., WADT 1997, LNAI 1376, 333–348. Springer, 1998.Google Scholar
  15. 15.
    T. Mossakowski. CASL: From semantics to tools. In S. Graf and M. Schwartzbach, eds., TACAS 2000, LNAI 1785, 93–108. Springer-Verlag, 2000.Google Scholar
  16. 16.
    T. Mossakowski. Heterogeneous development graphs and heterogeneous borrowing. In M. Nielsen (Ed.) Proceedings of Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, Springer LNAI, 2002.Google Scholar
  17. 17.
    T. Nipkow. Personal communication.Google Scholar
  18. 18.
    L. C. Paulson. Isabelle-A Generic Theorem Prover. LNAI 828. Springer, 1994.Google Scholar
  19. 19.
    Wolfgang Reif: The KIV-approach to Software Verification, In KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report, LNAI 1009, 339–368. Springer, 1995.Google Scholar
  20. 20.
    D. Sannella, A. Tarlecki. Specifications in an arbitrary institution, Information and Computation, 76(2–3):165–210, 1988.CrossRefMathSciNetzbMATHGoogle Scholar
  21. 21.
    D. Sannella, A. Tarlecki. Towards Formal Development of Programs from Algebraic Specifications: Model-Theoretic Foundations, 19th ICALP, Springer, LNAI 623, 656–671, Springer-Verlag, 1992.Google Scholar
  22. 22.
    A. Schairer, D. Hutter: Short Paper: Towards an Evolutionary Formal Software Development, In Proceedings of ASE 2001, IEEE, November, 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Serge Autexier
    • 1
  • Till Mossakowski
    • 2
  1. 1.FR 6.2 InformatikSaarland UniversitySaarbrücken
  2. 2.BISSUniversity of BremenBremen

Personalised recommendations