1.1 --- a/doc-src/isac/CTP-userinterfaces.bib Mon Jan 10 12:36:39 2011 +0100
1.2 +++ b/doc-src/isac/CTP-userinterfaces.bib Tue Jan 11 08:03:23 2011 +0100
1.3 @@ -1,3 +1,26 @@
1.4 +@InProceedings{makarius:isa-scala-jedit,
1.5 + author = {Makarius Wenzel},
1.6 + title = {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
1.7 + booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
1.8 + year = {2010},
1.9 + editor = {C. Sacerdoti Coen and D. Aspinall},
1.10 + address = {Edinburgh, Scotland},
1.11 + month = {July},
1.12 + organization = {FLOC 2010 Satellite Workshop},
1.13 + note = {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
1.14 +}
1.15 +
1.16 +@Book{db:dom-eng,
1.17 + author = {Bj{\o}rner, Dines},
1.18 + title = {Domain Engineering. Technology Management, Research and Engineering},
1.19 + publisher = {JAIST Press},
1.20 + year = {2009},
1.21 + month = {Feb},
1.22 + series = {COE Research Monograph Series},
1.23 + volume = {4},
1.24 + address = {Nomi, Japan}
1.25 +}
1.26 +
1.27 @inproceedings{Haftmann-Nipkow:2010:code,
1.28 author = {Florian Haftmann and Tobias Nipkow},
1.29 title = {Code Generation via Higher-Order Rewrite Systems},
1.30 @@ -9,17 +32,6 @@
1.31 volume = {6009}
1.32 }
1.33
1.34 -@InProceedings{wenzel:isar,
1.35 - author = {Wenzel, Markus},
1.36 - title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
1.37 - booktitle = {Theorem Proving in Higher Order Logics},
1.38 - year = {1999},
1.39 - editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
1.40 - series = {LNCS 1690},
1.41 - organization = {12th International Conference TPHOLs'99},
1.42 - publisher = {Springer}
1.43 -}
1.44 -
1.45 @Manual{coq1999,
1.46 title = {The Coq Proof Assistant},
1.47 author = {Barras, B. and others},
2.1 --- a/doc-src/isac/CTP-userinterfaces.tex Mon Jan 10 12:36:39 2011 +0100
2.2 +++ b/doc-src/isac/CTP-userinterfaces.tex Tue Jan 11 08:03:23 2011 +0100
2.3 @@ -22,10 +22,16 @@
2.4 \abstract{
2.5 TODO}
2.6
2.7 -\section{Introduction}\label{intro} (WN)
2.8 - 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.},
2.9 +\section{Introduction}\label{intro}
2.10 +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.
2.11
2.12 -graphical user interfaces (GUI)
2.13 +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.
2.14 +
2.15 +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.
2.16 +
2.17 +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}.
2.18 +
2.19 +\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.
2.20
2.21 %Georg
2.22 \section{State of the art in CTP Interfaces}
2.23 @@ -276,7 +282,7 @@
2.24 receive: def receive[R](f: PartialFunction[Any, R]): R
2.25 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]. \\
2.26 react:
2.27 -$$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing$$
2.28 +$$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
2.29 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]. \\
2.30 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. \\
2.31 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.\\