Userinterfaces for Computer Theorem Provers Feasibility Study in theISAC-Projekt
Marco Steger · 2011
The computer theorem prover Isabelle switches from a user interface for expert users to a user interface which is more powerful and which serves integration of Isabelle into other tools for software engineers. This bachelor thesis in “Telematik” introduces the specific components underlying Isabelle’s new user interface, the scala-layer for asyncronous editing of proof documents, the Java-based editor jEdit together with the respective plugin mechanisms; and the thesis documents the current organization of these components in Isabelle and sets up the whole system, Isabelle, Scala and jEdit in the IDE NetBeans copying the configuration of the Isabelle developer team. This setup is explored in the implementation of a test-plugin, and the experiences are documented in detail. Thus the prerequisites are given for cooperation in the further development of Isabelle’s future front-end and respective integration into development tools like test case generators for software engineers.