Abstract
We introduce the Casl Consistency Checker (CCC), a tool that supports consistency proofs in the algebraic specification language Casl. CCC is a faithful implementation of a previously described consistency calculus. Its system architecture combines flexibility with correctness ensured by encapsulation in a type system. CCC offers tactics, tactical combinators, forward and backward proof, and a number of specialised static checkers, as well as a connection to the Casl proof tool HOL-Casl to discharge proof obligations. We demonstrate the viability of CCC by an extended example taken from the Casl standard library of basic datatypes.
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.
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
Aspinall, D.: Proof general: A generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 38–42. Springer, Heidelberg (2000)
Baumeister, H., Bert, D.: Algebraic specification in Casl. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods: An Overview Using a Case Study, Springer, Heidelberg (2000)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)
Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)
The CCC homepage, http://www.informatik.uni-bremen.de/cofi/ccc
Coquand, C.: Agda homepage, http://www.cs.chalmers.se/~catarina/agda
Gimblett, A., Roggenbach, M., Schlingloff, H.: Towards a formal specification of an electronic payment system in CSP-CASL. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 61–78. Springer, Heidelberg (2005)
Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)
Hallgren, T.: Alfa homepage, http://www.cs.chalmers.se/~hallgren/Alfa
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall, Englewood Cliffs (1990)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. Design Automation, pp. 530–535. ACM, New York (2001)
Mossakowski, T.: CASL - from semantics to tools. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 93–108. Springer, Heidelberg (2000)
Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Roggenbach, M., Schröder, L.: Towards trustworthy specifications I: Consistency checks. In: Cerioli, M., Reggio, G. (eds.) WADT 2001 and CoFI WG Meeting 2001. LNCS, vol. 2267, pp. 305–327. Springer, Heidelberg (2002)
Spivey, M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lüth, C., Roggenbach, M., Schröder, L. (2005). CCC – The Casl Consistency Checker. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds) Recent Trends in Algebraic Development Techniques. WADT 2004. Lecture Notes in Computer Science, vol 3423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31959-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-31959-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25327-3
Online ISBN: 978-3-540-31959-7
eBook Packages: Computer ScienceComputer Science (R0)