Accession Number : ADA307301

Title :   Xlsabelle: A Graphical User Interface to the Isabelle Theorem Prover.

Descriptive Note : Research rept.,

Corporate Author : DEFENCE SCIENCE AND TECHNOLOGY ORGANIZATION CANBERRA (AUSTRALIA)

Personal Author(s) : Cant, A. ; Ozols, M. A.

PDF Url : ADA307301

Report Date : DEC 1995

Pagination or Media Count : 57

Abstract : Interactive theorem provers such as Isabelle are powerful tools, but are difficult and time-consuming to learn. If a suitable Graphical User Interface (GUI) is provided for such a tool, it can speed up the learning process considerably, leading to greater productivity for users of the tool, and increased takeup in industry. In this paper, we discuss the user-interface aspects of Isabelle, and formulate requirements for a GUI. XIsabelle, a GUI for XIsabelle, is described in detail. XIsabelle uses standard, easily available, methods for providing X Windows wrappers to interactive non-GUI programs, namely Tcl/Tk and the program Expect.

Descriptors :   *COMPUTER GRAPHICS, *MAN COMPUTER INTERFACE, *COMPUTER PROGRAM VERIFICATION, DATA BASES, COMPUTER PROGRAM DOCUMENTATION, SOFTWARE ENGINEERING, SYSTEMS ENGINEERING, DATA MANAGEMENT, COMPUTER AIDED DESIGN, REASONING, COMPUTER LOGIC, PROGRAMMING LANGUAGES, MATHEMATICAL LOGIC, INPUT OUTPUT PROCESSING, SYSTEMS ANALYSIS, INTERACTIVE GRAPHICS, COMPUTER FILES, COMPUTER AIDED INSTRUCTION, AUSTRALIA, OBJECT ORIENTED PROGRAMMING.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE