Integrating HOL-CASL into the Development Graph Manager MAYA
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.
KeywordsSource Node Theorem Prover Target Node Proof Obligation Proof Tree
Unable to display preview. Download preview PDF.
- 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.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
- 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.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.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.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.D. Hutter: Management of change in structured verification, In Proceedings Automated Software Engineering (ASE-2000), IEEE, 2000.Google Scholar
- 9.D. Hutter et. al. Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 523–530, 1996.Google Scholar
- 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.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
- 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.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.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.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.T. Nipkow. Personal communication.Google Scholar
- 18.L. C. Paulson. Isabelle-A Generic Theorem Prover. LNAI 828. Springer, 1994.Google Scholar
- 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
- 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.A. Schairer, D. Hutter: Short Paper: Towards an Evolutionary Formal Software Development, In Proceedings of ASE 2001, IEEE, November, 2001.Google Scholar