doc-src/isac/CTP-userinterfaces.tex
branchdecompose-isar
changeset 38113 ece09eca1d43
parent 38112 f49671358ddb
child 38114 7f4cfec6b910
equal deleted inserted replaced
38112:f49671358ddb 38113:ece09eca1d43
   170 Prooflanguage Isar is strutured such, that different parts can be interpreted in parallel. For instance, some might employ an 
   170 Prooflanguage Isar is strutured such, that different parts can be interpreted in parallel. For instance, some might employ an 
   171 an automated prover for some minutes, while the user wants to proceed with other parts of the same proof.
   171 an automated prover for some minutes, while the user wants to proceed with other parts of the same proof.
   172 A well-established concept able to cope with such parallel processing in actors, as introduced by Erlang.
   172 A well-established concept able to cope with such parallel processing in actors, as introduced by Erlang.
   173 This will be discussed in more detail in Sect. \ref{actors}
   173 This will be discussed in more detail in Sect. \ref{actors}
   174 
   174 
   175 \newpage
   175 
   176 %Andreas
   176 %Andreas
   177 \section{Isabelle's plans for new user-interfaces}\label{gui-plans}
   177 \section{Isabelle's plans for new user-interfaces}\label{gui-plans}
   178 %       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
   178 
   179 %       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
   179 The following observations lead to novel requirements for CTPS' userinterface:
   180 %
       
   181 %theorem proving will be integrated into software development
       
   182 %
       
   183 %hundreds of proof obligations are generated during a software verification process 
       
   184 %
       
   185 %so the final goald of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE).
       
   186 %
       
   187 %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.
       
   188 
   180 
   189 \begin{itemize}
   181 \begin{itemize}
   190 \item theorem proving will be integrated into software development
   182 \item theorem proving will be integrated into software development
   191 \item hundreds of proof obligations are generated during a software verification process
   183 \item hundreds of proof obligations are generated during a software verification process
   192 \item so the final goal of Isabelle's planning is integration with other software development tolls in an integrated development environment (IDE)
   184 \item so the final goal of Isabelle's planning is integration with other software development tolls in an integrated development environment (IDE)
   193 \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
   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
   194 \item favorite IDE is the jEdit, because it is clearer than Eclipse or NetBeans. The reason behind this choice follows in section 4.2
   186 \item favorite IDE is the jEdit, because it is clearer than Eclipse or NetBeans. The reason behind this choice follows in section \ref{plugin}
   195 \end{itemize}
   187 \end{itemize}
       
   188 
       
   189 These indicate design decisiouns are sketched in the sequel.
   196 
   190 
   197 \subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
   191 \subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
   198 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 user interfaces, 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.
   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 user interfaces, 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.
   199 
   193 
   200 
   194 
   209 \>\>type calcstate\\
   203 \>\>type calcstate\\
   210 \>\>type step = formula * position * tactic\\
   204 \>\>type step = formula * position * tactic\\
   211 \>\> \\
   205 \>\> \\
   212 \>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\
   206 \>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\
   213 \>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\
   207 \>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\
   214 \>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)\\
   208 \>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)
   215 %\\
       
   216 %\>\>val get\_next : program $\rightarrow$ calcstate $\rightarrow$ step\\
       
   217 %\>\>val get\_applicable\_tactics : program $\rightarrow$ calcstate $\rightarrow$ tactic list\\
       
   218 %\>\>val get\_intermediate : program $\rightarrow$ calcstate $\rightarrow$ position * position $\rightarrow$ step list\\
       
   219 \>end
   209 \>end
   220 \end{tabbing}}
   210 \end{tabbing}}
   221 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.
   211 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.
   222 
   212 
   223 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}.
   213 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}.
   224 
   214 
   225 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.
   215 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.
   226 %
   216 
   227 %\paragraph{Example: an object-oriented wrapper} as required for embedding the above mathematics engine into an object-oriented system. Such a wrapper looks like this:
   217 \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:
   228 %
   218 
   229 %TODO
   219 \begin{verbatim}
       
   220    public class Calcstate
       
   221    {
       
   222      private Program program_;
       
   223      private Tree<Step> calcstate_;
       
   224      private Position position_;
       
   225      
       
   226      public Calcstate(Program program) {...}
       
   227      public Step do_next() {...}
       
   228      public List<Step> apply_tactic(Tactic tactic) {...}
       
   229      public List<Step> apply_formular(Formular formular) {...}
       
   230    }
       
   231 \end{verbatim} 
   230 
   232 
   231 \subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
   233 \subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
   232 {\em new} %language --- what for, ideas ...
   234 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}.
   233 Scala is a hybrid multi-paradigm 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.\\
   235 
   234 Scala is pure object-oriented, this means every value is an object. 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 behaviors of objects are described by classes and traits [wiki]. 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. \\
   236 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 behaviors 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.
   235 In Scala every function is a value, hence Scala is also a functional language. 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[wiki-11-1s]. Furthermore Scala supports higher-order functions, currying and allows functions to be nested. \\
   237 
   236 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:
   238 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.
   237 \\
   239 
       
   240 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)}:
       
   241 
   238 \begin{itemize}
   242 \begin{itemize}
   239 \item generic classes
   243 \item generic classes
   240 \item variance annotations
   244 \item variance annotations
   241 \item upper and lower type bounds
   245 \item upper and lower type bounds
   242 \item classes and abstract types as object members
   246 \item classes and abstract types as object members
   243 \item compound types
   247 \item compound types
   244 \item explicitly typed self references
   248 \item explicitly typed self references
   245 \item views
   249 \item views
   246 \item polymorphic methods
   250 \item polymorphic methods
   247 \end{itemize}
   251 \end{itemize}
   248 Static types need no explicit declaration but can be given to give the code some clarity.\\\\
   252 
   249 Scala supports threads, but the Scala library contains an actor model inspired from Erlang. Concurrency and Scala actors follow in the next section.\\
   253 Static types need no explicit declaration but can be given to give the code some clarity.
   250 
   254 
   251 %quellen
   255 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.
   252 %%http://de.wikipedia.org/wiki/Scala_%28Programmiersprache%29
       
   253 %%http://en.wikipedia.org/wiki/Scala_%28programming_language%29
       
   254 %%http://creativekarma.com/ee.php/weblog/comments/why_scala_instead_of_java/
       
   255 %%http://www.scalasolutions.com/scala
       
   256 
       
   257 
   256 
   258 \subsection{Support for parallel processing}\label{actors}
   257 \subsection{Support for parallel processing}\label{actors}
   259 %actors copied from erlang
   258 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.
   260 
   259 
   261 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. \\
   260 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 behavior, an actor is able to reply to a message. The actor-based process is combined with pattern matching for messages.
   262 A very attractive model, because of the fact that it might addresses multicore processors and several techniques which are basically concurrent, is message-based concurrency. Most of the message passing systems, which are used in practice, are based on the actor model. \\
   261 
   263 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 several producers and one consumer, which are other actors. Actors share data by sending Messages which are sent asynchronously. Messages are unchangeable, so they don't require a lock and are used for communication between actors. By creating new actors, by sending messages to known actors, or changing its behavior, an actor is able to reply to a message. The actor-based process is combined with pattern matching for messages.\\
   262 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.
   264 The Erlang programming language is a functional programming language and a very popular implementation of 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 [IoC]. These systems use a very lightweight implementation and a large number of concurrent processes, which can active simultaneously.\\
   263 
   265 Operating system threads and threads of virtual machines, are too heavyweight for the implementation of such processes. The standard concurrency for mainstream platforms where shared-memory threads with locks. Such a platform is the Java Virtual Machine (JVM), which suffers from high memory consumption and context-switching overhead.
   264 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.
   266 The main reasons are:
   265 The most disadvantageous consequences are \cite{scala:jmlc06}:
   267 \begin{enumerate}
   266 \begin{enumerate}
   268 \item quick exhaustion of virtual address space
   267 \item quick exhaustion of virtual address space
   269 \item locking mechanisms often lack suitable contention managers
   268 \item locking mechanisms often lack suitable contention managers
   270 \end{enumerate}
   269 \end{enumerate}
   271 %[IoC]
   270 
   272 For that reasons Erlang uses lightweight concurrent processes by its own run time system and not by the underlying operating system [IoC] and the computations on these platforms are often modeled in an event-driven style, which is complicated and error-prone.
   271 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 modeled in an event-driven style, which is complicated and error-prone.
   273 \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.
   272 \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.
   274 
   273 
   275 \subparagraph{Thread-based implementation:} The behavior of a concurrent process is defined by implementing a thread-specific method. The execution state is maintained by an associated thread stack [2.P].
   274 \subparagraph{Thread-based implementation:} The behavior 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}.
   276 Supports blocking operations and can be executed on multicore processors in parallel.
   275 Supports blocking operations and can be executed on multicore processors in parallel.
   277 
   276 
   278 \subparagraph{Event-based implementation:} The behavior 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 [2.P]. Targets to a large number of actor which can be active simultaneously, because they are more lightweight.
   277 \subparagraph{Event-based implementation:} The behavior 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.
   279 
   278 
   280 \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 concurrent process implementation models, mentioned above and they are compatible with normal Virtual Machine 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.
   279 \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.
   281 
   280 
   282 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 operations are receive and react. An actor can suspend with a full thread stack (receive) or it can suspend with just a continuation closure (react) [2.P]. 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.
   281 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.
   283 
   282 
   284 receive:         def receive[R](f: PartialFunction[Any, R]): R
   283 \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:
   285 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. 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 behavior is therefore a sequential program which corresponds to thread-based programming [2.P]. \\
   284 $$\mathit{def}\;\mathit{receive}\mathit{[R]}(f: \mathit{PartialFunction}[Any, R]): \mathit{R}$$
   286 react:          
   285 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 behavior is therefore a sequential program which corresponds to thread-based programming \cite{Haller:2009:SAU:1496391.1496422}.
       
   286 \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:
   287 $$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
   287 $$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
   288 The action which is specified in the partial function is the last code that the current actor executes, if the message is matching. 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 [2.P]. \\
   288 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}. 
   289 For this implementation multiple acotrs 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. \\
   289 
   290 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.\\
   290 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.
   291 Event-Based Programming without Inversion of Control - Philipp Haller, Martin Odersky  [IoC]\\
   291 
   292 Scala actors: Unifying thread-based and event-based programming - Philipp Haller, Martin Odersky [2.P]\\
   292 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}.
   293 
       
   294 
   293 
   295 % Marco
   294 % Marco
   296 \section{Planned contributions at TU Graz}
   295 \section{Planned contributions at TU Graz}
   297 
   296 
   298 \subsection{Make Isabelle process structured derivations}\label{struct-der}
   297 \subsection{Make Isabelle process structured derivations}\label{struct-der}
   319 This plan involves the following details.
   318 This plan involves the following details.
   320 
   319 
   321 \subsection{Add a plug-in to jEdit}\label{plugin}
   320 \subsection{Add a plug-in to jEdit}\label{plugin}
   322     % file structure, copied from example project ...
   321     % file structure, copied from example project ...
   323 %Die von jEdit verfolgte Strategie im Bezug auf Plugin-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. Plugins lassen sich sehr einfach anfügen und durch die riesige Vielfalt von bereits bestehenden Plugins ist auch die Adaption von Plugins möglich bzw. zu empfehlen, denn warum sollte nicht bereits funktionierender Code verwendet werden?\\
   322 %Die von jEdit verfolgte Strategie im Bezug auf Plugin-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. Plugins lassen sich sehr einfach anfügen und durch die riesige Vielfalt von bereits bestehenden Plugins ist auch die Adaption von Plugins möglich bzw. zu empfehlen, denn warum sollte nicht bereits funktionierender Code verwendet werden?\\
   324 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 Plugin. There are a lot of useful and powerful Plugins available in the net and it is also possible to use a existing Plugin as part of a new one. Because of this facts, jEdit is very suitable for a project like Isabelle and also for the Isac-project at TU-Graz. \\\\
   323 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 Plugin. There are a lot of useful and powerful Plugins available in the net and it is also possible to use a existing Plugin 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.
   325 Each jEdit-Plugin 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 Plugin and provides information like the name, author, ... of the Plugin. 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 Plugin routines located in the source files. As you see, this files are used as interface between the Plugin and the jEdit engine itself.\\
   324 
       
   325 Each jEdit-Plugin\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 Plugin and provides information like the name, author, ... of the Plugin. 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 Plugin routines located in the source files. As you see, this files are used as interface between the Plugin and the jEdit engine itself.
       
   326 
   326 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.    
   327 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.    
   327 To get more information about the jEdit infrastructure see: http://jedit.org/users-guide/plugin-intro
   328 
   328 \\\\
   329 
   329 %isabell plugin beschreiben!!!!!!!!
   330 %isabell plugin beschreiben!!!!!!!!
   330 The Isabelle-team also follow use this Plugin-structure. In the next paragraph the involved files will be described. The jEdit-Isabelle-Plugin consists of:
   331 The Isabelle-team also follow use this Plugin-structure. In the next paragraph the involved files will be described. The jEdit-Isabelle-Plugin consists of:
   331 \begin{itemize}
   332 \begin{itemize}
   332 \item 14 Scala-source-files
   333 \item 14 Scala-source-files
   333 \item three XML-files
   334 \item 3 XML-files
   334 \item one property file
   335 \item 1 property file
   335 \end{itemize}
   336 \end{itemize}
   336 %Das vom Isabelle-Team erstellte jEdit-Plugin folgt natürlich auch dem oben erklärten Muster. Es wird nun genauer auf dieses Plugin eingegangen. The plugin consits of 14 scala-source-files, three xml-files and one property-file. 
   337 %Das vom Isabelle-Team erstellte jEdit-Plugin folgt natürlich auch dem oben erklärten Muster. Es wird nun genauer auf dieses Plugin eingegangen. The plugin consits of 14 scala-source-files, three xml-files and one property-file. 
   337 The property-file \textit{Isabelle.props} contains general informations about the Isabelle-Plugin and the needed dependencies between Isabelle and the other used Plugins like sidekick. \\
   338 \begin{description}
   338 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 Plugin.\\
   339 \item[Isabelle.props] The property-file \textit{Isabelle.props} contains general informations about the Isabelle-Plugin and the needed dependencies between Isabelle and the other used Plugins like sidekick.
   339 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.\\
   340 \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 Plugin.
   340 The last XML-file is \textit{services.xml} and is used to create instances of needed jEdit-Plugins.\\
   341 \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.
   341 This four files are located in the folder \textit{plugin}.\\\\
   342 \item[services.xml] The last XML-file is \textit{services.xml} and is used to create instances of needed jEdit-Plugins.
   342 The more interesting files, the scala-files of the Plugin, 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: \\
   343 \end{description}
   343 The file \textit{plugin.scala} is the main-file of the Isabelle-Plugin 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-Plugin should have this methods because they are very important for the handling of the Plugin! \\
   344 This four files are located in the folder \textit{plugin}.\\
   344 jEdit and also the Isabelle Plugin 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 individualize 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}.\\
   345 
   345 The next interesting file is \textit{scala-console.scala} with the main-class Scala-Console. This class is used to expand the Console-Plugin in a way, that it is possible to interpret Scala-code with a Shell inside of jEdit.\\ 
   346 The more interesting files, the scala-files of the Plugin, 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: 
   346 The file \textit{isabelle-sidekick.scala} is related to the file \textit{scala-console.scala} because it is also used to adapt the Plugin Sidekick for Isabelle.\\
   347 \begin{description}
   347 The files \textit{document-model.scala} and \textit{document-view.scala1} are used to connect the jEdit-buffer/the text-area to Isabelle. Both classes offer, upon others, methods to activate and deactivate this features.\\
   348 \item[plugin.scala] The file \textit{plugin.scala} is the main-file of the Isabelle-Plugin 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-Plugin should have this methods because they are very important for the handling of the Plugin!
   348 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-Plugin should be set up and the remaining files are not as important for the Isabelle-Plugin-structure:
   349 \item[dockable.scala] jEdit and also the Isabelle Plugin 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 individualize 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}.
   349 \begin{itemize}
   350 \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-Plugin in a way, that it is possible to interpret Scala-code with a Shell inside of jEdit.
   350 \item $html_panel.scala$
   351 \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 Plugin Sidekick for Isabelle.
   351 \item $isabelle_encoding.scala$
   352 \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.
   352 \item $isabelle_hyperlinks.scala$
   353 \end{description}
   353 \item $isabelle_options.scala$
   354 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-Plugin should be set up and the remaining files are not as important for the Isabelle-Plugin-structure.
   354 \item $isabelle_token_maker.scala$
   355 %\begin{itemize}
   355 \item $isabelle_hyperlinks.scala$
   356 %\item $html_panel.scala$
   356 \end{itemize}
   357 %\item $isabelle_encoding.scala$
       
   358 %\item $isabelle_hyperlinks.scala$
       
   359 %\item $isabelle_options.scala$
       
   360 %\item $isabelle_token_maker.scala$
       
   361 %\item $isabelle_hyperlinks.scala$
       
   362 %\end{itemize}
   357 
   363 
   358 
   364 
   359 %  Like each other jEdit-Plugin also this 
   365 %  Like each other jEdit-Plugin also this 
   360 
   366 
   361 %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.\\
   367 %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.\\
   396 \item $	\langle copy $file="plugin/Isabelle.props" todir="\${build.classes.dir}" $/\rangle$
   402 \item $	\langle copy $file="plugin/Isabelle.props" todir="\${build.classes.dir}" $/\rangle$
   397 \item $	\langle /target\rangle$
   403 \item $	\langle /target\rangle$
   398 \end{itemize}
   404 \end{itemize}
   399 %* kurze aufzählung der xml-netbeans-files + erklärung\\
   405 %* kurze aufzählung der xml-netbeans-files + erklärung\\
   400 \subsubsection{NetBeans project files}
   406 \subsubsection{NetBeans project files}
   401 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 informations 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!).\\
   407 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 informations 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!).
   402 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{pre-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.\\
   408 
       
   409 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{pre-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.
       
   410 
   403 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.
   411 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.
   404 
   412 
   405 \subsection{Use interfaces between Java and Scala}\label{java-scala}
   413 \subsection{Use interfaces between Java and Scala}\label{java-scala}
   406 %     how are data exchanged between Scala and Java ...
   414 %     how are data exchanged between Scala and Java ...
   407 jEdit is completely written in Java and the required plugin(s) for Isac 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.\\
   415 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.
   408 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.\\
   416 
   409 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} to work with a Java-button. But you can also use the Scala-equivalent \textit{scala.swing.Button}. This two button-types will provide nearly the same functionality.\\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.\\
   417 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.
       
   418 
       
   419 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.
       
   420 
       
   421 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.
   410 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:
   422 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:
   411 \begin{enumerate}
   423 \begin{enumerate}
   412 \item \textit{import javax.swing.JButton}
   424 \item \textit{import javax.swing.JButton}
   413 \item \textit{import scala.swing.Button}
   425 \item \textit{import scala.swing.Button}
   414 \item \textit{var b: scala.swing.Button}
   426 \item \textit{var b: scala.swing.Button}
   415 \item \textit{var jb: javax.swing.JButton}
   427 \item \textit{var jb: javax.swing.JButton}
   416 \item \textit{jb = b.peer}
   428 \item \textit{jb = b.peer}
   417 \end{enumerate}
   429 \end{enumerate}
   418 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! 
   430 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! 
   419 %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. ...
   431 %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. ...
   420 http://www.scala-lang.org/api/current/scala/swing/Button.html\\
       
   421 http://download.oracle.com/javase/1.4.2/docs/api/javax/swing/JButton.html
       
   422 
       
   423 \section{Conclusion and future work}
   432 \section{Conclusion and future work}
   424 
   433 
   425 
   434 
   426 \bibliography{CTP-userinterfaces}
   435 \bibliography{CTP-userinterfaces}
   427 %\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
   436 %\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}