Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

InterACT. An interactive theorem and completeness prover for algebraic specifications with conditional equations

 
: Klar, M.; Geisler, R.; Cornelius, F.

Wirsing, M.; Nivat, M.:
Algebraic methodology and software technology. Proceedings
Berlin: Springer, 1996 (Lecture Notes in Computer Science 1101)
ISBN: 3-540-61463-X
ISSN: 0302-9743
pp.563-566
International Conference on Algebraic Methodology and Software Technology (AMAST) <5, 1996, München>
English
Conference Paper
Fraunhofer ISST ()
algebraic specification; sufficient completeness; theorem proving

Abstract
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 InterAcr are described in this paper. Ideas for the design of user interfaces for interactive theorem provers can be found.

: http://publica.fraunhofer.de/documents/PX-19563.html