| branch | decompose-isar |
| changeset 38112 | f49671358ddb |
| parent 38111 | c185d9f262d1 |
| child 38113 | ece09eca1d43 |
| 38111:c185d9f262d1 | 38112:f49671358ddb |
|---|---|
18 TU Graz} |
18 TU Graz} |
19 |
19 |
20 \begin{document} |
20 \begin{document} |
21 \maketitle |
21 \maketitle |
22 \abstract{ |
22 \abstract{ |
23 TODO} |
23 This paper accompanies a pre-study on a sub-project planned within the \sisac-project. The goal of this sub-project is to extend ther userinterface of the theorem prover Isabelle such, that Structured Derivations according to R.J.Back are interactively processed. The sub-project is one step towards using the upcoming Isabelle/Isar/Scala layer for /sisac. |
24 |
|
25 The paper comprises three parts: (1) Ample space is given to background information about the state of the art in user interfaces for theorem provers and about the upcoming requirements for future developments. (2) focuses the strategy of Isabelle, the motivations and first decision. (3) provides a protocol of preparatory work for the sub-project. |
|
26 |
|
27 By the way, this paper shall serve as an entry point for students interested in joining the \sisac-team.} |
|
24 |
28 |
25 \section{Introduction}\label{intro} |
29 \section{Introduction}\label{intro} |
26 Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations. |
30 Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations. |
27 |
31 |
28 The present shift of the predominant user group from academic experts to software engineers raises novel user requirements for graphical user interfaces (GUI) of CTP. CTPs will become components of integrated development environments, and the knowledge bases have to scale up to industrial size. |
32 The present shift of the predominant user group from academic experts to software engineers raises novel user requirements for graphical user interfaces (GUI) of CTP. CTPs will become components of integrated development environments, and the knowledge bases have to scale up to industrial size. |
112 \end{figure} |
116 \end{figure} |
113 |
117 |
114 |
118 |
115 %(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html) |
119 %(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html) |
116 \subsubsection{Proof General for Isabelle} |
120 \subsubsection{Proof General for Isabelle} |
117 Proof General is a generic front-end for proof assistants \cite{aspinall}, based on the text editor Emacs. |
121 Proof General is a generic front-end for proof assistants \cite{Aspinall:2007:FIP:1420412.1420429}, based on the text editor Emacs. |
118 It has been developed at the University of Edinburgh with contributions from other sites. |
122 It has been developed at the University of Edinburgh with contributions from other sites. |
119 Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO. |
123 Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO. |
120 It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. |
124 It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. |
121 The communication between the user and the theorem prover takes place via two or more Emacs text widgets. |
125 The communication between the user and the theorem prover takes place via two or more Emacs text widgets. |
122 Therefore the user sees only the output from the latest proof step. |
126 Therefore the user sees only the output from the latest proof step. |
129 \begin{figure}[htbp] |
133 \begin{figure}[htbp] |
130 \centering |
134 \centering |
131 \includegraphics[scale=0.25]{fig/pgisabelle} |
135 \includegraphics[scale=0.25]{fig/pgisabelle} |
132 \caption{Proof General for Isabelle}% |
136 \caption{Proof General for Isabelle}% |
133 \end{figure} |
137 \end{figure} |
134 \newpage |
138 |
135 \subsubsection{Isabelle/Jedit} |
139 \subsubsection{Isabelle/Jedit} |
136 jEdit is a text editor for programmers, written in Java. |
140 jEdit is a text editor for programmers, written in Java. |
137 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much |
141 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much |
138 smaller and better focused on its primary task of text editing. |
142 smaller and better focused on its primary task of text editing. |
139 The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs \cite{makarius:isa-scala-jedit}. |
143 The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs \cite{makarius:isa-scala-jedit}. |