Publica
Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten. InterACT. An interactive theorem and completeness prover for algebraic specifications with conditional equations
| Haveraaen, M.; Owe, O.; Dahl, O.-J.:
Recent trends in data type specification 1996. Selected papers
Berlin: Springer, 1996 (Lecture Notes in Computer Science 1130)
ISBN: 3-540-61629-2
ISSN: 0302-9743
pp.291-305 |
| Workshop on Specification of Abstract Data Types <11, 1995, Oslo>
COMPASS Workshop <8, 1995, Oslo> |
|
| 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.