20 \begin{document} |
20 \begin{document} |
21 \maketitle |
21 \maketitle |
22 \abstract{ |
22 \abstract{ |
23 TODO} |
23 TODO} |
24 |
24 |
25 \section{Introduction}\label{intro} (WN) |
25 \section{Introduction}\label{intro} |
26 Computer theorem proving (CTP)\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.}, |
26 Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations. |
27 |
27 |
28 graphical user interfaces (GUI) |
28 The present shift of the predominant user group from academic experts to software engineers raises novel user requirements for graphical user interfaces (GUI) of CTP. CTPs will become components of integrated development environments, and the knowledge bases have to scale up to industrial size. |
|
29 |
|
30 Two issues are particularly challenging: First, the knowledge bases (containing specifications, programs, tests etc) are under joint construction of many engineers. So requirements concerning cooperative work arise as already known from distributed repositories and version management. |
|
31 |
|
32 Second, CTP tends to exhaust resources in memory and in runtime. 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}. |
|
33 |
|
34 \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 requiremtns 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 particularily 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. |
29 |
35 |
30 %Georg |
36 %Georg |
31 \section{State of the art in CTP Interfaces} |
37 \section{State of the art in CTP Interfaces} |
32 |
38 |
33 \subsection{A European technology: Coq and Isabelle}\label{ctp-techn} |
39 \subsection{A European technology: Coq and Isabelle}\label{ctp-techn} |
274 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. |
280 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. |
275 |
281 |
276 receive: def receive[R](f: PartialFunction[Any, R]): R |
282 receive: def receive[R](f: PartialFunction[Any, R]): R |
277 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]. \\ |
283 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]. \\ |
278 react: |
284 react: |
279 $$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing$$ |
285 $$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$ |
280 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]. \\ |
286 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]. \\ |
281 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. \\ |
287 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. \\ |
282 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.\\ |
288 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.\\ |
283 Event-Based Programming without Inversion of Control - Philipp Haller, Martin Odersky [IoC]\\ |
289 Event-Based Programming without Inversion of Control - Philipp Haller, Martin Odersky [IoC]\\ |
284 Scala actors: Unifying thread-based and event-based programming - Philipp Haller, Martin Odersky [2.P]\\ |
290 Scala actors: Unifying thread-based and event-based programming - Philipp Haller, Martin Odersky [2.P]\\ |