doc-isac/CTP-userinterfaces.tex
author wneuper <Walther.Neuper@jku.at>
Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787 26037efefd61
parent 60586 007ef64dbb08
permissions -rwxr-xr-x
Doc/Specify_Phase 2: copy finished
neuper@38077
     1
\documentclass{article}
neuper@38077
     2
\usepackage{a4}
neuper@38077
     3
\usepackage{times}
neuper@38077
     4
\usepackage{latexsym}
neuper@38077
     5
\bibliographystyle{alpha}
neuper@38077
     6
\usepackage{graphicx}
neuper@38077
     7
neuper@38077
     8
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@38077
     9
\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
neuper@38077
    10
\def\Problem{ {\tt Problem }}
neuper@38077
    11
neuper@38091
    12
\title{Userinterfaces for Computer Theorem Provers.\\
neuper@38091
    13
	Contributions to Isabelle
neuper@38077
    14
}
neuper@38077
    15
neuper@38077
    16
\author{G. Schafhauser, A. Schulhofer, M. Steger\\
neuper@38077
    17
Knowledge Management Institute (KMI)\\
neuper@38077
    18
TU Graz}
neuper@38077
    19
neuper@38077
    20
\begin{document}
neuper@38077
    21
\maketitle
neuper@38077
    22
\abstract{
Walther@60586
    23
This paper accompanies a where_-study on a sub-project planned within the \sisac-project. The goal of this sub-project is to extend the 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.
neuper@38112
    24
neuper@38114
    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 and decisions in order to cope with future requirements. (3) provides a protocol of preparatory work for the sub-project.
neuper@38112
    26
neuper@38114
    27
By the way, this paper shall serve as an entry point for students interested in joining the the work propared.}
neuper@38077
    28
neuper@38096
    29
\section{Introduction}\label{intro}
neuper@38096
    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.
neuper@38077
    31
neuper@38096
    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.
neuper@38096
    33
neuper@38114
    34
Two issues are particularly challenging: First, future knowledge bases (containing specifications, programs, tests etc) will under joint construction of many engineers. So requirements concerning cooperative work arise as already known from distributed repositories and version management.
neuper@38096
    35
neuper@38114
    36
Second, CTP tends to exhaust resources in memory and in run-time. So, CTP will take profit from multicore processors upcoming in this decade --- and CTP are best suited to meet the architectural challenges raised by parallel programming, since this kind of mathematics assistants generally follow rigorous architectural principles and are comparably easy to adapt to these challenges \cite{makarius:isa-scala-jedit}.
neuper@38096
    37
neuper@38114
    38
\medskip The paper is organised as follows: First a survey on CTP is given, Sect.\ref{ctp-techn} introduces two prominent CTPs, Sect.\ref{gui-coq-isa} describes their present user interfaces and Sect.\ref{gui-requir} goes into details with the novel requirements mentioned. Then Isabelle's plans for re-designing the user interface are presented: Sect.\ref{ml-users} motivates the strategy of how to approach the users' world, Sect.\ref{scala-medi} describes the rather recent programming language Scala connecting the world of languages for mathematics with the users' world and Sect.\ref{actors} goes into details with Scala's actor library. Finally possible contributions of the \sisac-team at TUG are discussed and prerequisites for such contributions presented: Sect.\ref{struct-der} presents a format for calculations particularly appropriate for education, which requires CTP support, Sect.\ref{plugin} describes plug-in technology required and Sect.\ref{netbeans} notes crucial details of proper project set-up in an integrated development environment.
neuper@38077
    39
neuper@38077
    40
%Georg
neuper@38077
    41
\section{State of the art in CTP Interfaces}
neuper@38077
    42
neuper@38077
    43
\subsection{A European technology: Coq and Isabelle}\label{ctp-techn}
neuper@38089
    44
%     http://en.wikipedia.org/wiki/Coq\\
neuper@38089
    45
%     http://coq.inria.fr/
neuper@38089
    46
%
neuper@38089
    47
%     http://en.wikipedia.org/wiki/Isabelle\_(theorem\_prover)\\
neuper@38089
    48
%     http://isabelle.in.tum.de/index.html
neuper@38089
    49
%
neuper@38089
    50
%why math -- functional: some of the languages have been specifically designed for constructing software for symbolic computation (SC). 
neuper@38089
    51
%%+ required for \ref{ml-users}
neuper@38089
    52
%
neuper@38089
    53
%SC http://en.wikipedia.org/wiki/Symbolic\_computation
neuper@38089
    54
%% mainly does not compute numerical values, but terms containing variables like functions (symbols)
neuper@38089
    55
%
neuper@38089
    56
%The LCF project
neuper@38089
    57
%http://hopl.murdoch.edu.au/showlanguage.prx?exp=8177
neuper@38089
    58
%specifically designed a 'meta language' (ML)
neuper@38089
    59
%http://en.wikipedia.org/wiki/ML\_(programming\_language)
neuper@38089
    60
%\cite{pl:milner97}
neuper@38089
    61
%for developing CTP
neuper@38089
    62
\subsubsection{Standard ML}
georg@38107
    63
Standard ML is a general-purpose, modular, functional programming language \cite{pl:milner97}.
neuper@38089
    64
Programs written in Standard ML consist of expressions to be evaluated, as opposed to statements or commands. 
neuper@38114
    65
Functional programming languages constitute a family very different of object orientated languages, see Sect. \ref{ml-users}. ML originated from the LCF-project(Logic for Computable Functions)\cite{meta-Ml}, where it had been developed as a meta language. Since ML has been standardised this family of language is called Standard ML. Important for the logical foundation of SML is the $\lambda$-calculus.
georg@38103
    66
%http://en.wikipedia.org/wiki/Standard_M 
neuper@38089
    67
\subsubsection{Coq}
georg@38103
    68
Coq is an interactive theorem prover, developed in France.
georg@38103
    69
It is programmed in Objective Caml, an ML based programming language.
georg@38103
    70
It has the ability to express  mathematical  assertions and check proof of mathematical assertions. 
neuper@38089
    71
Furthermore Coq includes automatic theorem proving tactics and decision procedures.
georg@38105
    72
Properties, programs and proofs are written a functional programming language called the Calculus of Inductive Constructions (CIC).
georg@38107
    73
Proof development in Coq is done through a language of tactics that allows a user-guided proof process \cite{coq1999}.
neuper@38089
    74
Another feature of Coq is “that it can automatically extract executable programs from specifications, as either Objective Caml 
neuper@38089
    75
or Haskell source code.“
georg@38103
    76
There are many easy-to-read introductions to Coq \footnote{http://coq.inria.fr/a-short-introduction-to-coq} on the internet.
neuper@38089
    77
\subsubsection{Isabelle}
neuper@38091
    78
Isabelle is an interactive theorem proving framework for high-level natural deduction proofs \cite{Paulson:Isa94}, written in Standard ML. 
neuper@38114
    79
Isabelle is developed at University of Cambridge, Technische Universit\"at M\"unchen
neuper@38114
    80
and Universit\'e Paris-Sud. Isabelle is called a framework, because it implements several object logics.
georg@38105
    81
The most widespread logic of Isabelle is Isabelle/HOL, short for higher-order logic.
neuper@38114
    82
Isabelle/HOL includes several  specification tools, e.g. for data-types, inductive definitions and functions with complex pattern matching.
georg@38107
    83
Proofs are written in the structured proof language Isar \cite{wenzel:isar}.Isabelle implements several tools, e.g. a reasoner, a simplifier and powerful automatic provers(Sledgehammer), increase the user's productivity in theorem proving. 
neuper@38089
    84
Isabelle provides notational support: new notations can be introduced, using normal mathematical symbols.
neuper@38114
    85
Definitions and proofs may include \LaTeX{} source, from which Isabelle can automatically generate typeset documents.
georg@38107
    86
Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell \cite{Haftmann-Nipkow:2010:code}.
georg@38107
    87
%(http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html)
neuper@38089
    88
\subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa}
neuper@38089
    89
%     CoqIDE, ..
neuper@38089
    90
%         http://coq.inria.fr/what-is-coq?q=node/57\\
neuper@38089
    91
%         earlier than Isabelle/jEdit
neuper@38089
    92
%
neuper@38089
    93
%     ProofGeneral for Isabelle
neuper@38089
    94
%         http://proofgeneral.inf.ed.ac.uk/\\
neuper@38089
    95
%         emacs stone age ?
neuper@38089
    96
\subsubsection{Coq Integrated Development Environment}
georg@38107
    97
CoqIDE\footnote{http://coq.inria.fr/V8.1/refman/Reference-Manual016.html}, short for Coq Integrated Development Environment, is a graphical interface for Coq. It is written in Ocaml.
neuper@38114
    98
Its main purpose is to allow the user to navigate forward and backward into a Coq file, 
neuper@38089
    99
executing corresponding commands or undoing them respectively. 
neuper@38089
   100
There are several  buffers for helping to write proof scripts.
neuper@38089
   101
Among all these buffers, there is always one which is the current running buffer, whose name is displayed on a green background,
georg@38107
   102
which is the one where Coq commands are currently executed.  
georg@38107
   103
CoqIDE provides also a feedback system for the user. 
neuper@38114
   104
Therefore the background is green when a command succeeds, otherwise an error message is displayed in the message window and the error location is underlined red.
neuper@38089
   105
CoqIDE offers only basic editing commands, therefore it is possible to launch another more sophisticated text editor. 
neuper@38089
   106
Furthermore CoqIde provides a proof wizard “for automatically trying to solve the current goal using simple tactics.”
neuper@38114
   107
Another features of this IDE are the customisation options, which can be accessed by the Edit menu. 
neuper@38114
   108
This allows the user to change the appearance of the IDE.
neuper@38077
   109
neuper@38077
   110
neuper@38089
   111
\begin{figure}[htbp]
neuper@38089
   112
\centering
neuper@38089
   113
%\includegraphics[bb=0 0 10 10]{coqide.png}
neuper@38114
   114
\includegraphics[scale=0.20]{fig/coqide}
neuper@38089
   115
\caption{CoqIDE main screen}
neuper@38089
   116
\end{figure}
neuper@38077
   117
neuper@38077
   118
georg@38107
   119
%(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
neuper@38089
   120
\subsubsection{Proof General for Isabelle}
neuper@38112
   121
Proof General is a generic front-end for proof assistants \cite{Aspinall:2007:FIP:1420412.1420429}, based on the text editor Emacs.
georg@38107
   122
It has been developed at the University of Edinburgh with contributions from other sites.
georg@38107
   123
Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO.
georg@38107
   124
It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. 
georg@38107
   125
The communication between the user and the theorem prover takes place via two or  more Emacs text widgets.
georg@38107
   126
Therefore the user sees only the output from the latest proof step.
neuper@38077
   127
neuper@38077
   128
georg@38107
   129
Isabelle/Isar\footnote{http://proofgeneral.inf.ed.ac.uk/} Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General. 
neuper@38089
   130
There is full support for Unicode Tokens, using the Isabelle print mode for X Symbol tokens. Many Isabelle theories have X Symbol syntax already defined 
neuper@38089
   131
and it's easy to add to your own theories. 
georg@38107
   132
%(http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME)
neuper@38089
   133
\begin{figure}[htbp]
neuper@38089
   134
\centering
neuper@38114
   135
\includegraphics[scale=0.30]{fig/pgisabelle}
neuper@38089
   136
\caption{Proof General for Isabelle}%
neuper@38089
   137
\end{figure}
neuper@38112
   138
neuper@38089
   139
\subsubsection{Isabelle/Jedit}
neuper@38089
   140
jEdit is a text editor for programmers, written in Java.
neuper@38114
   141
Compared to fully-featured IDEs, such as Eclipse or NetBeans, jEdit is much 
neuper@38089
   142
smaller and better focused on its primary task of text editing.
neuper@38114
   143
The general look of the Isabelle/jEdit plug-in is similar to existing Java IDEs \cite{makarius:isa-scala-jedit}.
neuper@38114
   144
The main Isabelle/jEdit plug-in consists of ten small Scala files that augment some key jEdit components in order to provide a metaphor of asynchronous proof document editing. 
neuper@38114
   145
Isabelle/jEdit integrates the jEdit 4.3.2 framework  and some further  jEdit plug-ins. 
neuper@38114
   146
It also implements custom-made 'IsabelleText Unicode' font that actually contains the usual Isabelle symbols that users expect from long 
georg@38107
   147
years of Proof General X-Symbol support.
neuper@38089
   148
The editor provides useful feedback, via semantic information from the processed document in the background. 
georg@38107
   149
A lot of information can be directly attached 
neuper@38114
   150
to the source text, via colouring, tool-tips, pop-ups etc.
neuper@38077
   151
neuper@38077
   152
\subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir}
neuper@38089
   153
%     @ interaction close to tty (Telegraph)\\
neuper@38089
   154
%       BUT: separate parts in {\em one} proof could be processed in parallel
neuper@38089
   155
%
neuper@38089
   156
%     @ http://www.informatik.uni-bremen.de/uitp/
neuper@38089
   157
%
neuper@38089
   158
%     @ ... see\\
neuper@38089
   159
%       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
neuper@38089
   160
%       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
neuper@38114
   161
"After several decades, most proof assistants are still centred around TTY-based interaction in a
georg@38107
   162
tight read-eval-print loop.
georg@38107
   163
All Emacs-based GUI's for CTPs follow this synchronous
neuper@38089
   164
model based on single commands with immediate response, meaning that the editor waits for the
georg@38107
   165
prover after each command", according to \cite{makarius:isa-scala-jedit}. As to multicore politics of leading semiconductor chip manufacturer, parallelism in software technology has become an issue.
georg@38107
   166
Therefore the support of parallelism in CTP technology improves the performance and multiuser support.
georg@38107
   167
%So it is necessary to use proof documents instead of proof scripts.  
georg@38107
   168
%Proof scripts are  sequences of commands however proof documents are structured texts. 
georg@38107
   169
%So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. 
neuper@38114
   170
Proof language Isar is structured such, that different parts can be interpreted in parallel. For instance, some might employ an 
georg@38107
   171
an automated prover for some minutes, while the user wants to proceed with other parts of the same proof.
georg@38107
   172
A well-established concept able to cope with such parallel processing in actors, as introduced by Erlang.
georg@38107
   173
This will be discussed in more detail in Sect. \ref{actors}
neuper@38110
   174
andreas@38113
   175
neuper@38077
   176
%Andreas
neuper@38114
   177
\section{Isabelle's plans for new userinterfaces}\label{gui-plans}
andreas@38113
   178
andreas@38113
   179
The following observations lead to novel requirements for CTPS' userinterface:
neuper@38077
   180
neuper@38089
   181
\begin{itemize}
neuper@38089
   182
\item theorem proving will be integrated into software development
neuper@38089
   183
\item hundreds of proof obligations are generated during a software verification process
neuper@38114
   184
\item so the final goal of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE)
neuper@38089
   185
\item still many principal issues need to be clarified with respect to integration of CTP and other development tools. So engaging into details makes no sense at the present, and Isabelle will approach the final goal via experimental intermediate steps of integration
neuper@38114
   186
\item favourite IDE is jEdit, because it is clearer than Eclipse or NetBeans. The reason behind this choice follows in section \ref{plugin}
neuper@38089
   187
\end{itemize}
neuper@38077
   188
neuper@38114
   189
These indicate design decisions are sketched in the sequel.
andreas@38113
   190
neuper@38077
   191
\subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
neuper@38114
   192
In Sect.\ref{ctp-techn} reasons have been given, why mathematics software at the state-of-the-art cannot be written in Java or the like. On the other side, Sect.\ref{gui-requir} stated requirements for mathematical userinterfaces, which cannot be accomplished by ML-like languages. These requirements can be best accomplished by languages like Java, which have powerful libraries available for convenient assembly of GUIs.
neuper@38089
   193
neuper@38077
   194
\paragraph{Example: a functional mathematics engine} as the experimental one in the \sisac-project is given by the following signature:
neuper@38077
   195
{\it
neuper@38077
   196
\begin{tabbing}
neuper@38077
   197
\=xx\=xxxxxxxxxxxxxxxxxxxxxxxxx\=\kill
neuper@38077
   198
\>signature INTERPRETER =\\
neuper@38077
   199
\>sig\\
neuper@38077
   200
\>\>type calcstate\\
neuper@38077
   201
\>\>type step = formula * position * tactic\\
neuper@38077
   202
\>\> \\
neuper@38077
   203
\>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\
neuper@38077
   204
\>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\
neuper@38114
   205
\>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)\\
neuper@38077
   206
\>end
neuper@38077
   207
\end{tabbing}}
neuper@38077
   208
The three essential functions are \textit{do\_next}, which reads a \textit{program} for determining the next \textit{step} in a calculation, the function \textit{apply\_tactic}, which applies a \textit{tactic} input by the user to the current \textit{position} in a calculation and thus may produce a list of \textit{step}s and the function \textit{apply\_formula}, which applies an input \textit{formula} accordingly.
neuper@38077
   209
neuper@38077
   210
Now, the point with functional programming is, that the functions do {\em not} cause persistent updates in some memory, rather: all three functions above take the current state of the calculation, \textit{calcstate}, as an argument and after they have done they work return the updated \textit{calcstate}.
neuper@38077
   211
neuper@38077
   212
There are several advantages of this kind of programming: more straight forward verification, which is not discussed here, and other features. For instance, given the three functions above, it is easy to undo steps of calculations, or go back to an earlier step of calculations: one just needs to store the \textit{calcstate}s (in a list), even without knowing the details of the \textit{calcstate}, which thus can be encapsulated for internal access only.
andreas@38113
   213
andreas@38113
   214
\paragraph{Example: an object-oriented wrapper} as required for embedding the above mathematics engine into an object-oriented system. Such a wrapper may look like this:
neuper@38114
   215
{\footnotesize
andreas@38113
   216
\begin{verbatim}
andreas@38113
   217
   public class Calcstate
andreas@38113
   218
   {
andreas@38113
   219
     private Program program_;
andreas@38113
   220
     private Tree<Step> calcstate_;
andreas@38113
   221
     private Position position_;
andreas@38113
   222
     
andreas@38113
   223
     public Calcstate(Program program) {...}
andreas@38113
   224
     public Step do_next() {...}
andreas@38113
   225
     public List<Step> apply_tactic(Tactic tactic) {...}
andreas@38113
   226
     public List<Step> apply_formular(Formular formular) {...}
andreas@38113
   227
   }
andreas@38113
   228
\end{verbatim} 
neuper@38114
   229
}
neuper@38077
   230
\subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
andreas@38113
   231
Scala \footnote{http://www.scala-lang.org} is a hybrid programming language. It combines object-oriented programming and functional programming. Scala runs on the Java Virtual Machine and is byte-code compatible with existing Java programs. The compilation model of Scala is nearly the same as the Java's model. So existing tools, libraries and applications can be used with Scala. The syntax of Scala is similar to Java and ML. A number of keywords plus the block syntax is adopted from Java and from ML the syntax for type annotation and declaration. The source-code is typically reduced, concisely and more compact compared to equivalent Java code \footnote{http://www.scalasolutions.com/scala}.
andreas@38113
   232
neuper@38114
   233
Scala is pure object-oriented, this means every value is an object \cite{odersky:scala06}. The same is true for primitive data types, because compiler-generated byte code is using primitive data types. Known design patterns from OOP can be used with Scala as well. "Data types and behaviours of objects are described by classes and traits" \footnote{http://en.wikipedia.org/wiki/Scala\_(programming\_language)}. Traits not only consist of definitions, they also can contain implementations of methods. To avoid the problems of multiple inheritance, classes are able to extend various traits, this is a flexible mixin-based mechanism. The keyword Object is used to implement a Singleton-Class.
andreas@38113
   234
andreas@38113
   235
In Scala every function is a value, hence Scala is also a functional language \cite{odersky:scala06}. Functions in Scala are first-class objects, this means it is possible to pass a function as a parameter, return a function from a subroutine, or assign to a variable. Scala also supports case classes, which are used for pattern matching. Case classes are regular classes which export their constructor parameters \footnote{http://de.wikipedia.org/wiki/Scala\_(Programmiersprache)}. Furthermore Scala allows functions to be nested.
andreas@38113
   236
andreas@38113
   237
Scala is more statically typed than Java, but is able to infer types by usage. So most static type declarations are optional. This static type system ensures a safe and coherent use of abstraction. Scala supports \footnote{http://en.wikipedia.org/wiki/Scala\_(programming\_language)}:
andreas@38113
   238
neuper@38089
   239
\begin{itemize}
neuper@38089
   240
\item generic classes
neuper@38089
   241
\item variance annotations
neuper@38089
   242
\item upper and lower type bounds
neuper@38089
   243
\item classes and abstract types as object members
neuper@38089
   244
\item compound types
neuper@38089
   245
\item explicitly typed self references
neuper@38089
   246
\item views
neuper@38089
   247
\item polymorphic methods
neuper@38089
   248
\end{itemize}
neuper@38089
   249
andreas@38113
   250
Static types need no explicit declaration but can be given to give the code some clarity.
neuper@38089
   251
andreas@38113
   252
Scala supports threads, but the Scala library contains an actor model inspired from Erlang \cite{armstrong:erlang96}. Concurrency and Scala actors follow in the next section.
neuper@38077
   253
neuper@38077
   254
\subsection{Support for parallel processing}\label{actors}
neuper@38114
   255
Concurrency has lately become more and more attention, because multicore processors make concurrency very important for efficient program execution, by running multiple threads parallel and so concurrent programming gets indispensable and distributed computing, web services and mobile environments are naturally concurrent. A very attractive model is message-based concurrency, which is based on the actor model.
neuper@38089
   256
neuper@38114
   257
An actor is a concurrent process that executes a function. The state of an actor gets never shared, so it doesn't need to compete for locks of shared data. Actors own a mailbox where incoming messages are stored in. A mailbox is mainly a queue with actors, which operate as several producers and one consumer. Actors share data by sending messages which are sent asynchronously. Messages are unchangeable, so they don't require a lock. By creating new actors, by sending messages to known actors, or changing its behaviour, an actor is able to reply to a message. The actor-based process is combined with pattern matching for messages.
andreas@38113
   258
andreas@38113
   259
The Erlang programming language is a functional programming language that supports message-based concurrency, which operates with actors. It was developed for real-time control systems. Such systems are telephone exchanges, network simulators and distributed resource controllers \cite{scala:jmlc06}. These systems use a very popular lightweight implementation and a large number of concurrent processes, which can be active simultaneously.
andreas@38113
   260
andreas@38113
   261
Operating system threads and threads of virtual machines are too heavyweight for the implementation of such processes. The standard concurrency for mainstream platforms were shared-memory threads with locks. Such a platform is the Java Virtual Machine (JVM), which suffers from high memory consumption and context-switching overhead.
andreas@38113
   262
The most disadvantageous consequences are \cite{scala:jmlc06}:
neuper@38089
   263
\begin{enumerate}
neuper@38091
   264
\item quick exhaustion of virtual address space
neuper@38091
   265
\item locking mechanisms often lack suitable contention managers
neuper@38089
   266
\end{enumerate}
andreas@38113
   267
neuper@38114
   268
For that reasons Erlang uses lightweight concurrent processes by its own run time system and not by the underlying operating system \cite{scala:jmlc06} and the computations on these platforms are often modelled in an event-driven style, which is complicated and error-prone.
neuper@38091
   269
\paragraph{Two different strategies for concurrency} are being used for implementation. This two strategies often follow different programming models, the benefit of thread-based models is that they are easier to use, but they still suffer from the memory consumption and the context-switching. The event-based models are just the opposite of the thread-based, they are more efficient, but in massive designs they are very difficult.
neuper@38091
   270
neuper@38114
   271
\subparagraph{Thread-based implementation:} The behaviour of a concurrent process is defined by implementing a thread-specific method. The execution state is maintained by an associated thread stack \cite{Haller:2009:SAU:1496391.1496422}.
neuper@38091
   272
Supports blocking operations and can be executed on multicore processors in parallel.
neuper@38091
   273
neuper@38114
   274
\subparagraph{Event-based implementation:} The behaviour is defined by a number of (non-nested) event-handlers which are called from inside an event loop. The execution state of a concurrent process is maintained by an associated record or object \cite{Haller:2009:SAU:1496391.1496422}. Targets to a large number of actor which can be active simultaneously, because they are more lightweight.
neuper@38091
   275
andreas@38113
   276
\paragraph{Actors in Scala} are based on actors in Erlang. Scala uses the basic thread model of Erlang, but on the other hand all higher-level functions got implemented in the Scala library as classes or methods. The Scala-actors are a unification of the implementation models mentioned above and they are compatible with normal Virtual Machine (VM) thread. Normal VM threads can use the same communication and monitoring capabilities, because they are treated like an actor. A message-based concurrency seems to be more secure than shared-memory with locks, because accessing an actor's mailbox is race-free. The advantage of a implementation in a library is that it can be flexibly extended and adapted to new needs. The library makes use of Scala abstraction opportunities, like partial functions and pattern matching.
neuper@38091
   277
neuper@38114
   278
The main idea of this model is that an actor is able to wait for a message by using two different operations, which try to remove a message from the current actor's mailbox. To do so, a partial function must be given to the operation, that specifies a set of message patterns. These are {\itshape receive} and {\itshape react}. 'An actor can suspend with a full thread stack (receive) or it can suspend with just a continuation closure (react)' \cite{Haller:2009:SAU:1496391.1496422}. The first operation of an actor to wait for an message is equal to thread-based programming and the second operation to event-based programming.
neuper@38091
   279
andreas@38113
   280
\subparagraph{receive:} The current actor's mailbox get scanned and if there is one message which matches one of the patterns declared in the partial function, the message is removed from the mailbox and the partial function is applied to the message, the result is returned. The declaration of receive:
andreas@38113
   281
$$\mathit{def}\;\mathit{receive}\mathit{[R]}(f: \mathit{PartialFunction}[Any, R]): \mathit{R}$$
neuper@38114
   282
Otherwise the current thread blocks. Thus the receiving actor has the ability to execute normally when receiving a message which matches.  Note that receive retains the complete call stack of the receiving actor; the actor’s behaviour is therefore a sequential program which corresponds to thread-based programming \cite{Haller:2009:SAU:1496391.1496422}.
andreas@38113
   283
\subparagraph{react:} The action which is specified in the partial function is the last code that the current actor executes, if the message is matching. The declaration of react:
neuper@38096
   284
$$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
andreas@38113
   285
The partial function gets registered by the current actor and the underlying thread gets released. React has the return type Nothing, this means that the method never returns normally. When the actor receives a matching message, the earlier registered partial function gets called and the actor's execution gets continued. The partial function f which corresponds to a set of event handlers \cite{Haller:2009:SAU:1496391.1496422}. 
neuper@38089
   286
andreas@38113
   287
For this implementation multiple actors are executed by multiple threads and therefore a thread pool is used. Whenever it is necessary the pool can be re sized, to support the operations of the thread-based and event-based model. If only operations of the event-based model are executed then the thread pool could be fixed. To avoid system-included deadlocks, if some actors use thread-based operations, the thread pool has to grow, because if there are outstanding tasks and every worker thread is occupied by a blocked actor, new threads are necessary.
andreas@38113
   288
andreas@38113
   289
Since the communication between actors takes place through asynchronous message passing, asynchronous operations get executed, tasks have to be created and submitted to a thread pool for execution. A new task is created, when an actor spawns a new actor or a message, which enables an actor to continue, is send to an actor which is suspended in a react operation or by calling react, where a message can be immediately removed from the mailbox \cite{Haller:2009:SAU:1496391.1496422}.
neuper@38077
   290
neuper@38077
   291
% Marco
neuper@38077
   292
\section{Planned contributions at TU Graz}
neuper@38077
   293
neuper@38077
   294
\subsection{Make Isabelle process structured derivations}\label{struct-der}
neuper@38077
   295
Structured Derivations (SD) is a format for calculational reasoning, which has been established by \cite{back-grundy-wright-98}. This is an example calculation:
neuper@38077
   296
{\it\begin{tabbing}
neuper@38077
   297
123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
neuper@38077
   298
\> $\bullet$\> \Problem [ maximum\_by, calculus ]\\
neuper@38077
   299
\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$\\
neuper@38077
   300
\>\> $\bullet$\> \Problem [make, diffable, funtion]\\
neuper@38077
   301
\>\> \dots\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\
neuper@38077
   302
\>\> $\bullet$\> \Problem [on\_interval, for\_maximum, differentiate, function]\\
neuper@38077
   303
\>\>\> $\vdash$\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\
neuper@38077
   304
\>\>\> $\bullet$\> \Problem [differentiate, funtion]\\
neuper@38077
   305
\>\>\> \dots\> $\overline{A}^\prime(\alpha) = 8\cdot r^2\cdot(-(\sin\alpha)^2+(\cos\alpha)^2 - 2\cdot\sin\alpha\cdot\cos\alpha)$\\
neuper@38077
   306
\>\>\> $\bullet$\> \Problem [on\_interval, goniometric, equation]\\
neuper@38077
   307
\>\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\
neuper@38077
   308
\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\
neuper@38077
   309
\>\> $\bullet$\> \Problem [tool, find\_values]\\
neuper@38077
   310
\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ]\\
neuper@38077
   311
\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !
neuper@38077
   312
\end{tabbing}}
neuper@38077
   313
The plan is to use the machinery provided Isabelle/Isar as a 'logical operating system' ~\cite{isar-impl} and adapt the machinery such that is accepts SC in parallel to the Isar proof language~\cite{wenzel:isar}.
neuper@38077
   314
neuper@38077
   315
This plan involves the following details.
neuper@38077
   316
neuper@38077
   317
\subsection{Add a plug-in to jEdit}\label{plugin}
neuper@38089
   318
    % file structure, copied from example project ...
neuper@38114
   319
%Die von jEdit verfolgte Strategie im Bezug auf plug-in Management und natürlich generell die totale Offenlegegung des Codes ist für ein Projekt wie Isabelle und auch für das Isac-Project an der TU ideal. plug-ins lassen sich sehr einfach anfügen und durch die riesige Vielfalt von bereits bestehenden plug-ins ist auch die Adaption von plug-ins möglich bzw. zu empfehlen, denn warum sollte nicht bereits funktionierender Code verwendet werden?\\
neuper@38114
   320
The importance of connecting the ML-world with the world of user interfaces has been is discussed in Sect.\ref{ml-users}. jEdit follows these lines, it is an open-source, Java-based text editor that works on Windows, Mac OS X, and Linux. A big advantage of jEdit is, that there is a very good and also simple way to use and write a plug-in. There are a lot of useful and powerful plug-ins available in the net and it is also possible to use a existing plug-in as part of a new one. Because of this facts, jEdit is very suitable for a project like Isabelle and also for the \sisac-project at TU-Graz.
andreas@38113
   321
neuper@38114
   322
Each jEdit plug-in\footnote{To get more information about the jEdit infrastructure see: http://jedit.org/users-guide/plugin-intro} basically consists of source files, written in Java or Scala, XML-files and property files. The XML-Files are important for the administration of a plug-in and provides information like the name, author, ... of the plug-in. They are also containing small pieces of BeanShell code which is executed upon a user request. (Like pressing the 'start plugin' button.) So the XML-files provide the “glue” between user input and specific plug-in routines located in the source files. As you see, this files are used as interface between the plug-in and the jEdit engine itself.
andreas@38113
   323
neuper@38089
   324
Based on the jEdit API, you are allowed to design your code quit freely and don't have to use a prescribed way to implement your ideas.    
andreas@38113
   325
andreas@38113
   326
neuper@38089
   327
%isabell plugin beschreiben!!!!!!!!
neuper@38114
   328
The Isabelle-team also follow use this plug-in structure. In the next paragraph the involved files will be described. The jEdit-Isabelle plug-in consists of:
neuper@38089
   329
\begin{itemize}
georg@38105
   330
\item 14 Scala-source-files
andreas@38113
   331
\item 3 XML-files
andreas@38113
   332
\item 1 property file
neuper@38089
   333
\end{itemize}
neuper@38114
   334
%Das vom Isabelle-Team erstellte jEdit plug-in folgt natürlich auch dem oben erklärten Muster. Es wird nun genauer auf dieses plug-in eingegangen. The plugin consits of 14 scala-source-files, three xml-files and one property-file. 
andreas@38113
   335
\begin{description}
neuper@38114
   336
\item[Isabelle.props] The property-file \textit{Isabelle.props} contains general information about the Isabelle plug-in and the needed dependencies between Isabelle and the other used plug-ins like sidekick.
neuper@38114
   337
\item[dockables.xml] The XML-file \textit{dockables.xml} is used to create the needed dock-able windows which are important to set up the GUI of the plug-in.
neuper@38114
   338
\item[actions.xml] In the file \textit{actions.xml}, the dockable windows are added to the window-manager \textit{wm} and there is also some BeanShell-code to activate the Isabelle-GUI.
neuper@38114
   339
\item[services.xml] The last XML-file is \textit{services.xml} and is used to create instances of needed jEdit plug-ins.
andreas@38113
   340
\end{description}
andreas@38113
   341
This four files are located in the folder \textit{plugin}.\\
andreas@38113
   342
neuper@38114
   343
The more interesting files, the scala-files of the plug-in, can be found in the 'src/jedit'-directory. In this directory you can find the file \textit{Dummy.java} which is a dummy class and is simply used to make javadoc work. Just forget about this file. Also there is a folder/package \textit{jedit} which contains all Scala-source-files. Now it is time to take a closer look on the source-files: 
andreas@38113
   344
\begin{description}
neuper@38114
   345
\item[plugin.scala] The file \textit{plugin.scala} is the main-file of the Isabelle plug-in and there are two important parts. First the \textit{Isabelle object}. This object contains data like name and path and also few basic functions. The second part is the \textit{class Plugin} which is derived from EBPlugin. Here the basic methods \textit{handleMessage}, \textit{start} and \textit{stop} are implemented. Each jEdit plug-in should have this methods because they are very important for the handling of the plug-in!
neuper@38114
   346
\item[dockable.scala] jEdit and also the Isabelle plug-in work with dock-able windows. This means that you can move around each single window and dock it somewhere on the screen. So it is possible to customise the jEdit-GUI. To support this, the file \textit{dockable.scala} is needed. The file \textit{output-dockable.scala} is derived from \textit{dockable.scala} and is used to print the result/output in a dock-able window. The same thing with \textit{protocol-dockable.scala} and \textit{raw-output-dockable.scala}.
neuper@38114
   347
\item[scala-console.scala] The next interesting file is \textit{scala-console.scala} with the main-class Scala-Console. This class is used to expand the Console plug-in in a way, that it is possible to interpret Scala-code with a Shell inside of jEdit.
neuper@38114
   348
\item[isabelle-sidekick.scala] The file \textit{isabelle-sidekick.scala} is related to the file \textit{scala-console.scala} because it is also used to adapt the plug-in Sidekick for Isabelle.
andreas@38113
   349
\item[document-model.scala, document-view.scala] The files \textit{document-model.scala} and \textit{document-view.scala} are used to connect the jEdit-buffer/the text-area to Isabelle. Both classes offer, upon others, methods to activate and deactivate this features.
andreas@38113
   350
\end{description}
neuper@38114
   351
There also some other source-files but they aren’t discussed here, because the main goal of this paragraph is to give a basic idea how a jEdit plug-in should be set up and the remaining files are not as important for the Isabelle plug-in structure.
andreas@38113
   352
%\begin{itemize}
andreas@38113
   353
%\item $html_panel.scala$
andreas@38113
   354
%\item $isabelle_encoding.scala$
andreas@38113
   355
%\item $isabelle_hyperlinks.scala$
andreas@38113
   356
%\item $isabelle_options.scala$
andreas@38113
   357
%\item $isabelle_token_maker.scala$
andreas@38113
   358
%\item $isabelle_hyperlinks.scala$
andreas@38113
   359
%\end{itemize}
neuper@38089
   360
neuper@38089
   361
neuper@38089
   362
%  Like each other jEdit-Plugin also this 
neuper@38089
   363
neuper@38089
   364
%Das Konzept des frei wählbaren Designs ist am Beginn villeicht etwas schwierig umzusetzten, da es leichter ist, sich irgendwo anzulehnen bzw. ein bereits bestehendes sowie funktionierendes Konzept zu übernehmen. So wurden auch die ersten Schritte an der TU gemacht. Zu diesem Zweck wurde das von den Entwicklern von jEdit zur Verfügung gestellte plugin 'QuickNotepad' übernommen und in Scala übersetzt. Obwohl Scala eng mit Java verknüpft ist, war doch einiges an 'rewritting' notwendig bis das Scala-plugin lauffähig wurde. Die benötigten XML-files konnten dazu nahezu unberührt gelassen werden.\\
neuper@38077
   365
neuper@38077
   366
\subsection{Details of NetBeans projects}\label{netbeans}
neuper@38089
   367
%     Scala + Java: html project files
georg@38105
   368
As described in the last paragraph, jEdit is a open-source-project. The jEdit-developers use a NetBeans-project to produce the source-code and so it is beneficial to use a NetBeans project too, because there is a quite good documentation about setting up a NetBeans-project with the jEdit-source. See http://wiki.netbeans.org/NetbeansedJEdit for further information.\\\\
neuper@38114
   369
If you want to set up a new jEdit plug-in project you have to attend that you have to create some source-files and that there must be a connection to the jEdit-source because you will need to exchange data with the jEdit engine. This could probably look like: \textit{jEdit.getProperty("options.isabelle.isabelle")}\\
neuper@38114
   370
As shown above, the jEdit-source is needed to compile and build your plug-in. There are two ways to organise your project:
georg@38105
   371
\begin{itemize}
georg@38105
   372
\item with jEdit source code - two projects in one
georg@38105
   373
\item with jedit.jar library
georg@38105
   374
\end{itemize}
neuper@38114
   375
\subsubsection{Plug-in with jEdit-source}
neuper@38114
   376
It is a good way to download the jEdit source as NetBeans project because then it is possible to add another sub-project to the existing jEdit-NetBeans-project. As you see it is also possible to mix Scala and Java. A big advantage is, that debugging will now work really fine. If you want to set up a project like this, you should complete the following steps.
neuper@38089
   377
\begin{enumerate}
neuper@38114
   378
\item {Create a new NetBeans-project for your plug-in like \textit{example-plugin}. This will probably be a Scala-Project.}
neuper@38089
   379
\item Download (and try out) the \textit{jEdit-NetBeans-project}
neuper@38089
   380
\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at \textit{Libraries} $\rightarrow$ \textit{add Project...} and then choose the \textit{jEdit-NetBeans-project}.
neuper@38089
   381
\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at project-name-label $\rightarrow$ \textit{Properties} $\rightarrow$ \textit{Run} $\rightarrow$ \textit{Main Class:} org.gjt.sp.jedit.jEdit
neuper@38089
   382
\item compile and run
neuper@38089
   383
\end{enumerate}
neuper@38089
   384
neuper@38114
   385
\subsubsection{Plug-in with jedit.jar}
neuper@38089
   386
It is also possible to use the \textit{jedit.jar} file. This file is already included in \$ISABELLE-HOME/contrib/jedit-4.3.2. Now you just have to follow this steps:
neuper@38089
   387
\begin{enumerate}
neuper@38114
   388
\item {Create a new NetBeans-project for your plug-in like \textit{example-plugin}. This will probably be a Scala-Project.}
neuper@38089
   389
\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at \textit{Libraries} $\rightarrow$ \textit{add JAR/Folder...} and then choose the \textit{jedit.jar} file.
neuper@38089
   390
\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at project-name-label $\rightarrow$ \textit{Properties} $\rightarrow$ \textit{Run} $\rightarrow$ \textit{Main Class:} org.gjt.sp.jedit.jEdit
neuper@38089
   391
\item compile and run
neuper@38089
   392
\end{enumerate}
neuper@38114
   393
This are two different ways to get started. It is difficult to say what is better because both versions have advantages. Now it is time to start coding your own plug-in but there are still a few things to think about. Remember, that a plug-in consists of source-, XML- and property-files. On default, NetBeans will just pack the source-files in the \textit{example-plugin.jar}-package. So you have to add a copy/move-routine in the \textit{build.xml} file of your NetBeans-project to get a complemented package.
neuper@38089
   394
\begin{itemize}
Walther@60586
   395
\item $\langle target name="-where_-jar"\rangle$
neuper@38089
   396
\item $	\langle copy $file="plugin/services.xml" todir="\${build.classes.dir}" $/\rangle$
neuper@38089
   397
\item $	\langle copy $file="plugin/dockables.xml" todir="\${build.classes.dir}" $/\rangle$
neuper@38089
   398
\item $	\langle copy $file="plugin/actions.xml" todir="\${build.classes.dir}" $/\rangle$	
neuper@38089
   399
\item $	\langle copy $file="plugin/Isabelle.props" todir="\${build.classes.dir}" $/\rangle$
neuper@38089
   400
\item $	\langle /target\rangle$
neuper@38089
   401
\end{itemize}
neuper@38089
   402
%* kurze aufzählung der xml-netbeans-files + erklärung\\
neuper@38089
   403
\subsubsection{NetBeans project files}
neuper@38114
   404
As you see in the paragraph above, it is also important to have basic knowledge about NetBeans, the project structure and how to change the operational sequences. A typical NetBeans-project consist of the source- and library-files and administrative XML- and property-files. In this paragraph the administrative part of the project is of note. The most important file is \textit{build.xml}. This file can be found in the project directory. There is also a folder \textit{nbproject} which contains the remaining XML- and property-files and also a folder \textit{private}, where individual user information about the project is stored. The files in this \textit{private} folder are not important to describe (and they should not be pushed on the repository!).
andreas@38113
   405
Walther@60586
   406
A build-file like \textit{build.xml} contains one project and at least one (default) target. Targets contain task elements. Each task element of the build-file can have an id attribute and can later be referred to by the value supplied to this. So the id has to be unique. Such targets can be "run", "debug", "build", ... and can have dependencies to other targets. Tasks define what should happen, if a target is executed. So like in the example above, the target is \textit{where_-jar}, that means that this things will happen before the jar-package is packed. The tasks of this target are copying some files into the package.
andreas@38113
   407
neuper@38089
   408
The files inside the \textit{nbproject}-folder are not so important because some of it are generated from \textit{build.xml} and changes in this files are useless. Just the file project.properties is really interesting because this file gives a nice and tight overview about the project settings.
neuper@38077
   409
neuper@38077
   410
\subsection{Use interfaces between Java and Scala}\label{java-scala}
neuper@38089
   411
%     how are data exchanged between Scala and Java ...
andreas@38113
   412
jEdit is completely written in Java and the required plugin(s) for \sisac{ }will be coded in Scala - so there must be ways to exchange data between Java and Scala. One way is to connect this two worlds with the in 4.2 described XML-files. Here you need to use a third type of code to get an interface between Java and Scala code. But there is also a way to get a direct connection.
andreas@38113
   413
andreas@38113
   414
This link should be shown on the graphic-library \textit{Swing}. In both languages it is possible to use Swing which provides a lot of different shapes and useful functionality. So there is a Java-Swing and also a Scala-Swing-library. Now it is interesting to examine the connection between this two libraries.
andreas@38113
   415
andreas@38113
   416
In Scala a direct use of Java-Libs (like Java-Swing) is possible. So if you are Java-Programmer and want to use Java-Swing in Scala, you can simply type\\ \textit{import javax.swing.JButton}\footnote{http://download.oracle.com/javase/1.4.2/docs/api/javax/swing/JButton.html} to work with a Java-button. But you can also use the Scala-equivalent \textit{scala.swing.Button}\footnote{http://www.scala-lang.org/api/current/scala/swing/Button.html}. This two button-types will provide nearly the same functionality.
andreas@38113
   417
andreas@38113
   418
So what is the idea of creating a nearly similar library a second time? Why have the Scala-developers done such extra work? The answer is, that they have tried to improve and simplify the usage of the Swing-library(and many other libs too!). So big parts of this Scala-Libraries are just Wrapper-objects, Wrapper-Classes and Wrapper-Methods of already existing parts in Java-Libraries. Needless to say that they also added new useful shapes and functionality.
neuper@38089
   419
But there is one important question left: Is it possible to mix Scala- and Java-objects? And yes, it is possible. There is a really easy way to convert a Scala-object to the Java-equivalent:
neuper@38089
   420
\begin{enumerate}
neuper@38089
   421
\item \textit{import javax.swing.JButton}
neuper@38089
   422
\item \textit{import scala.swing.Button}
neuper@38089
   423
\item \textit{var b: scala.swing.Button}
neuper@38089
   424
\item \textit{var jb: javax.swing.JButton}
neuper@38089
   425
\item \textit{jb = b.peer}
neuper@38089
   426
\end{enumerate}
neuper@38114
   427
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 plug-in written in Scala and one coded in Java. With this connection between Scala and Java, it would be easy to connect this two plug-ins! 
neuper@38089
   428
%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. ...
neuper@38077
   429
\section{Conclusion and future work}
neuper@38114
   430
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.
neuper@38077
   431
neuper@38114
   432
The general background information 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 asynchronous processing of proof documents, the concept of actors.
neuper@38114
   433
neuper@38114
   434
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 which is: extend the theorem prover Isabelle with Structured Derivations.
neuper@38114
   435
neuper@38114
   436
This part is considered an appropriate to start realising this goal and to prepare for future work, which will join the \sisac-project with front-of-the-wave technology in computer theorem proving and respective userinterfaces.
neuper@38114
   437
neuper@38114
   438
\bigskip\noindent {\Large\textbf{Acknowledgements}}
neuper@38114
   439
neuper@38114
   440
\medskip\noindent 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.\\
neuper@38114
   441
The leader of the \sisac-project expresses his pleasure about the efficient collaboration between the institutes IICM and IST at TUG.
neuper@38077
   442
neuper@38079
   443
\bibliography{CTP-userinterfaces}
neuper@38079
   444
%\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
neuper@38077
   445
\end{document}