Abstract
CASL, the common algebraic specification language, has been developed as a language that subsumes many previous algebraic specification frameworks and also provides tool interoperability. CASL is a complex language with a complete formal semantics. It is therefore a challenge to build good tools for CASL. In this work, we present and discuss the Bremen HOL-CASL system, which provides parsing, static checking, conversion to LATEX and theorem proving for CASL specifications. To make tool construction manageable, we have followed some guidelines: re-use of existing tools, interoperability of tools developed at different sites, and construction of generic tools that can be used for several languages. We describe the structure of and the experiences with our tool and discuss how the guidelines work in practice.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
A. Aasa. Precedences in specifications and implementations of programming languages. Theoretical Computer Science, 142(1):3–26, May 1995. 98
D. Baillie. Proving theorems about CASL specifications. Talk at the 14th Workshop on Algebraic Development Techniques, Bonas, France, September 1999. 97, 102
M. Brand, H. Jong, P. Klint, and P. Olivier. Efficient Annotated Terms. Technical report, CWI, 1999. Accepted by SPE. 97
M. Cerioli, A. Haxthausen, B. Krieg-Brückner, and T. Mossakowski. Permissive subsorted partial logic in Casl. In M. Johnson, editor, Algebraic methodology and software technology: 6th international conference, AMAST 97, volume 1349 of Lecture Notes in Computer Science, pages 91–107. Springer-Verlag, 1997. 95, 98
M. Cerioli and J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173:311–347, 1997. 99
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. F. Quesada. The Maude system. In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), pages 240–243, Trento, Italy, July 1999. Springer-Verlag LNCS 1631. System Description. 103
CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible by WWW7 and FTP8. 107
CoFI Language Design Task Group. CASL — The CoFI Algebraic Specification Language — Summary. Documents/CASL/Summary, in [7], Oct. 1998. 93
CoFI Semantics Task Group. CASL — The CoFI Algebraic Specification Language — Semantics. Note S-9 (version 0.95), in [7], Mar. 1999. 93
CoFI Task Group on Tools. The CoFI-Tools group home page. http://www.loria.fr/~hkirchne/CoFI/Tools/index.html. 97
J. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Language, and Computation. Addison-Wesley, Reading, MA, 1979. 98
B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer, and A. Baer. The UniForM Workbench, a universal development environment for formal methods. In FM99: World Congress on Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1186–1205. Springer-Verlag, 1999. 105
P. G. Larsen. VDM and proof rules for underdetermined functions. Talk at the IFIP WG 1.3 meeting, Bonas, France, September 1999. 94
C. Lüth, H. Tej, Kolyang, and B. Krieg-Brückner. TAS and IsaWin: Tools for transformational program developkment and theorem proving. In J.-P. Finance, editor, Fundamental Approaches to Software Engineering FASE’99. Joint European Conferences on Theory and Practice of Software ETAPS’99, number 1577 in LNCS, pages 239–243. Springer Verlag, 1999. 103, 105
C. Lüth and B. Wolff. Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming, 9(2):167–189, Mar. 1999. 103, 105
J. Meseguer. General logics. In Logic Colloquium 87, pages 275–329. North Holland, 1989. 99
T. Mossakowski, Kolyang, and B. Krieg-Brückner. Static semantic analysis and theorem proving for CASL. In F. Parisi Presicce, editor, Recent trends in algebraic development techniques. Proc. 12th International Workshop, volume 1376 of Lecture Notes in Computer Science, pages 333–348. Springer, 1998. 94, 96, 98, 99
P. D. Mosses. CoFI: The Common Framework Initiative for Algebraic Specification and Development. In TAPSOFT’ 97: Theory and Practice of Software Development, volume 1214 of LNCS, pages 115–137. Springer-Verlag, 1997. Documents/Tentative/Mosses97TAPSOFT, in [7]. 93
P. D. Mosses. Formatting CASL specifications using LATEX. Note C-2, in [7], June 1998. 96
L. C. Paulson. Isabelle-A Generic Theorem Prover. Number 828 in LNCS. Springer Verlag, 1994. 99
C. Ringeissen. Demonstration of ELAN for rewriting in CASL specifications. Talk at the 14th Workshop on Algebraic Development Techniques, Bonas, France, September 1999. 97
M. Roggenbach and T. Mossakowski. Basic datatypes in CASL. Note M-6, in [7], Mar. 1999. 106
P. Y. Schobbens. Second-order proof systems for algebraic specification languages. In H. Ehrig and F. Orejas, editors, Recent Trends in Data Type Specification, volume 785 of Lecture Notes in Computer Science, pages 321–336, 1994. 101
A. Tarlecki. Moving between logical systems. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors, Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types, volume 1130 of Lecture Notes in Computer Science, pages 478–502. Springer Verlag, 1996. 99
A. Tarlecki. Towards heterogeneous specifications. In D. Gabbay and M. van Rijke, editors, Frontiers of Combining Systems, 2nd International Workshop. Research Studies Press, 1999. To appear. 106
M. van den Brand. CasFix — mapping from the concrete CASL to the abstract syntax in ATerms format. http://adam.wins.uva.nl/~markvdb/cofi/casl.html, 1998. 97
M. G. J. van den Brand and J. Scheerder. Development of parsing tools for CASL using generic language technology. Talk at the 14th Workshop on Algebraic Development Techniques, Bonas, France, September 1999. 97
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T. (2000). CASL: From Semantics to Tools. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_8
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive