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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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.
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.
M. Cerioli and J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173:311–347, 1997.
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.
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.
R. Diaconescu, J. Goguen, P. Stefaneas. Logical support for modularization, In G. Huet, G. Plotkin, (Eds), Logical Environments, 83–130, Cambridge Press 1991.
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.
D. Hutter: Management of change in structured verification, In Proceedings Automated Software Engineering (ASE-2000), IEEE, 2000.
D. Hutter et. al. Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 523–530, 1996.
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.
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.
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.
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.
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.
T. Mossakowski. CASL: From semantics to tools. In S. Graf and M. Schwartzbach, eds., TACAS 2000, LNAI 1785, 93–108. Springer-Verlag, 2000.
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.
T. Nipkow. Personal communication.
L. C. Paulson. Isabelle-A Generic Theorem Prover. LNAI 828. Springer, 1994.
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.
D. Sannella, A. Tarlecki. Specifications in an arbitrary institution, Information and Computation, 76(2–3):165–210, 1988.
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.
A. Schairer, D. Hutter: Short Paper: Towards an Evolutionary Formal Software Development, In Proceedings of ASE 2001, IEEE, November, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Autexier, S., Mossakowski, T. (2002). Integrating HOL-CASL into the Development Graph Manager MAYA . In: Armando, A. (eds) Frontiers of Combining Systems. FroCoS 2002. Lecture Notes in Computer Science(), vol 2309. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45988-X_2
Download citation
DOI: https://doi.org/10.1007/3-540-45988-X_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43381-1
Online ISBN: 978-3-540-45988-0
eBook Packages: Springer Book Archive