InterACT: An interactive theorem and completeness prover for algebraic specifications with conditional equations
The InterACT tool is an interactive theorem prover for algebraic specifications emphasizing user-friendliness. InterACT is integrated in the existing ACT environment. The main purpose of InterACT is to teach formal methods in universitary courses about formal specification of software systems. It has already been used successfully in this area.
The theoretical and practical concepts underlying InterACT are described in this paper. Ideas for the design of user interfaces for interactive theorem provers can be found.
Unable to display preview. Download preview PDF.
- 1.R. Bardohl. Concept and Implementation of the Language GVT for the Graphical Visualisation of Terms of Algebraic Specifications (in german). Master's thesis, Technische Universität Berlin, 1993.Google Scholar
- 2.I. Claßen. Compositionality of Application Oriented Structuring Mechanisms for Algebraic Specification Languages with Initial Semantics. PhD thesis, Technische Universität Berlin, 1993.Google Scholar
- 3.I. Claßen, H. Ehrig, and D. Wolz. Algberaic Specification Techniques and Tools for Software Development — The ACT Approach. AMAST Series in Computing Vol. 1. World Scientific, 1993.Google Scholar
- 4.H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, Berlin, 1985.Google Scholar
- 5.R. Geisler and M. Klar. Design and Realisation of the Interactive Theorem-and Completeness Prover InterACT for Algebraic Specifications (in german). Master's thesis, Technische Universität Berlin, June 1995.Google Scholar
- 6.M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In 10th International Conference on Automated Deduction. Springer LNCS 449, July 1990.Google Scholar
- 7.T. Langbacka, R. Ruksenas, and J. von Wright. TkWinHOL A Tool for Doing Window Inference in HOL. Technical report, Abo Akademi University, 1995.Google Scholar
- 8.L.C. Paulson. Logic and Computation. Cambridge University Press, 1987.Google Scholar
- 9.L.C. Paulson. Isabelle. Springer LNCS 828, 1994.Google Scholar
- 10.P. Robinson and J. Staples. Formalizing a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1), Feb. 1993.Google Scholar
- 11.J. Rumbaugh. Eine Betrachtung der Architektur Model-View-Controller (MVC) (in german). OBJEKTspektrum, 3, März 94.Google Scholar
- 12.D. Wolz. Design of a compiler for lazy pattern driven narrowing. In Proc. of the 7th International Workshop on the Specification of Abstract Data Types, LNCS 534. Springer, 1991.Google Scholar
- 13.D. Wolz. A tool for checking ADT completeness and consistency. In Proc. of the third LOTOSPHERE workshop, Pisa, 1992.Google Scholar
- 14.H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction prinziple for equational specifications. In E. Lusk and R. Overbeek, editors, 10th International Conference on Automated Deduction (LNCS 310). Springer, 1988.Google Scholar