18 TU Graz} |
18 TU Graz} |
19 |
19 |
20 \begin{document} |
20 \begin{document} |
21 \maketitle |
21 \maketitle |
22 \abstract{ |
22 \abstract{ |
23 |
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 |
24 |
25 } |
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.} |
26 |
28 |
27 \section{Introduction}\label{intro} |
29 \section{Introduction}\label{intro} |
28 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. |
29 |
31 |
30 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. |
170 Therefore the support of parallelism in CTP technology could improve the performance and the multiuser support. |
172 Therefore the support of parallelism in CTP technology could improve the performance and the multiuser support. |
171 So it is necessary to use proof documents instead of proof scripts. |
173 So it is necessary to use proof documents instead of proof scripts. |
172 Proof scripts are sequences of commands however proof documents are structured texts. |
174 Proof scripts are sequences of commands however proof documents are structured texts. |
173 So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. |
175 So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. |
174 (MW async-isabelle-scala.pdf) |
176 (MW async-isabelle-scala.pdf) |
175 \newpage |
177 |
176 %Andreas |
178 %Andreas |
177 \section{Isabelle's plans for new user-interfaces}\label{gui-plans} |
179 \section{Isabelle's plans for new user-interfaces}\label{gui-plans} |
178 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
180 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
179 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
181 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
180 % |
182 % |
429 \item \textit{var jb: javax.swing.JButton} |
431 \item \textit{var jb: javax.swing.JButton} |
430 \item \textit{jb = b.peer} |
432 \item \textit{jb = b.peer} |
431 \end{enumerate} |
433 \end{enumerate} |
432 As the example above illustrates, a conversion of Scala- to Java-objects is possible. It looks easy but also a little bit useless. Why should you need this? Just imagine that there is a Plugin written in Scala and one coded in Java. With this connection between Scala and Java, it would be easy to connect this two Plugins! |
434 As the example above illustrates, a conversion of Scala- to Java-objects is possible. It looks easy but also a little bit useless. Why should you need this? Just imagine that there is a Plugin written in Scala and one coded in Java. With this connection between Scala and Java, it would be easy to connect this two Plugins! |
433 %Diesen direkten Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing. Beide Sprachen stellen diese Grafik-Bibliotheken zur Verfügung (und darin auch eigene Shapes und Funktionalität). Es ist jedoch möglich, Java-Bibliotheken, wie eben auch Java-Swing in Scala zu verwenden. Ein JButton kann zum Beispiel mittels \textit{import javax.swing.JButton} eingebunden und damit sofort auch verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek zur Verfügung: \textit{scala.swing.Button}. Es wird nahezu die selbe Funktionalität angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht(???). Man kann sich nun fragen, warum sich die Scala-Entwickler einerseit die Mühe gemacht haben die Verwendung Java-Swing, wie in Java selbst, möglich zu machen und andererseits mit Scala-Swing eine nahezu idente Alternative geschaffen haben. Die Antwort darauf zeigt wie der objektorientierte Teil von Scala in vielen Bereichen aufgebaut wurden. Es wurde kein neues Konzept für diese Grafikklassen entworfen sondern Wrapper-Objekte/Methoden/Klassen erstellt, die das Arbeiten mit diesen Grafikkomponenten erleichtern soll. Ein Letztes Problem bleibt noch: Es ist zwar sehr einfach ein Java-Swing-Objekt an einen Scala-Swing-Container (zb. Frame) anzubinden, da eine Konvertierung von Java-Komponente in ein Scala-Äquivalent ist problemlos möglich. ... |
435 %Diesen direkten Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing. Beide Sprachen stellen diese Grafik-Bibliotheken zur Verfügung (und darin auch eigene Shapes und Funktionalität). Es ist jedoch möglich, Java-Bibliotheken, wie eben auch Java-Swing in Scala zu verwenden. Ein JButton kann zum Beispiel mittels \textit{import javax.swing.JButton} eingebunden und damit sofort auch verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek zur Verfügung: \textit{scala.swing.Button}. Es wird nahezu die selbe Funktionalität angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht(???). Man kann sich nun fragen, warum sich die Scala-Entwickler einerseit die Mühe gemacht haben die Verwendung Java-Swing, wie in Java selbst, möglich zu machen und andererseits mit Scala-Swing eine nahezu idente Alternative geschaffen haben. Die Antwort darauf zeigt wie der objektorientierte Teil von Scala in vielen Bereichen aufgebaut wurden. Es wurde kein neues Konzept für diese Grafikklassen entworfen sondern Wrapper-Objekte/Methoden/Klassen erstellt, die das Arbeiten mit diesen Grafikkomponenten erleichtern soll. Ein Letztes Problem bleibt noch: Es ist zwar sehr einfach ein Java-Swing-Objekt an einen Scala-Swing-Container (zb. Frame) anzubinden, da eine Konvertierung von Java-Komponente in ein Scala-Äquivalent ist problemlos möglich. ... |
|
436 |
434 \section{Conclusion and future work} |
437 \section{Conclusion and future work} |
|
438 This paper collected background information on the topic of userinterfaces for theorem provers, which is not covered by the standard curriculum at Graz University of Technology: Computer theorem proving, respective interfaces and novel challenges for userinterfaces raised by integration of CTP into software engineering tools within the current decade. |
|
439 |
|
440 The general background informations has been related to students' knowledge already gained during studies: functional and object-oriented programming paradigm, programming languages with focus on Scala and Scala's specific concept to handle asyncronous processing of proof documents, the concept of actors. |
|
441 |
|
442 An important part of the paper is a protocol of preparatory work already done on project-setup and software components required for the next goal: extend the theorem prover Isabelle with Structured Derivations. |
|
443 |
|
444 This part is considered an appropriate to start realising this goal preparing future work, which will join the \sisac-project with front-of-the-wave technology in computer theorem proving and respective userinterfaces. |
|
445 |
|
446 \bigskip textbf{Acknowledgements}\\ |
|
447 The authors thank the lecturer of 'Verfassen wissenschaftlicher Arbeiten' in winter semester 2010/11, Dipl.-Ing. Dr.techn. Markus Strohmaier, for his support on working on the topic they are interested in.\\ |
|
448 The leader of the \sisac-project expresses his pleasure about the efficient collaboration between the institutes IICM and IST at TUG. |
|
449 |
435 |
450 |
436 |
451 |
437 \bibliography{CTP-userinterfaces} |
452 \bibliography{CTP-userinterfaces} |
438 %\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl} |
453 %\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl} |
439 \end{document} |
454 \end{document} |