wneuper/isa: comparison doc-src/isac/CTP-userinterfaces.tex

equal deleted inserted replaced

-:4e128838c313
+:a1cc2a17498b
 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
 \def\Problem{ {\tt Problem }}
-\title{Upcoming Userinterfaces for Computer Theorem Provers.\\
+\title{Userinterfaces for Computer Theorem Provers.\\
-	The case of Isabelle
+	Contributions to Isabelle
 }
 \author{G. Schafhauser, A. Schulhofer, M. Steger\\
 Knowledge Management Institute (KMI)\\
 TU Graz}
 Properties, programs and proofs are written a language called the Calculus of Inductive Constructions (CIC).
 Coq is based on a type-checking algorithm, therefore Coq uses only typing judgements.
 Coq supports a functional programming language.
 (http://coq.inria.fr/a-short-introduction-to-coq)
 \subsubsection{Isabelle}
-Isabelle is an interactive theorem proving framework for high-level natural deduction proofs, written in Standard ML.
+Isabelle is an interactive theorem proving framework for high-level natural deduction proofs \cite{Paulson:Isa94}, written in Standard ML.
 Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow)
 and Université Paris-Sud (Makarius Wenzel).
 The most widespread instance of Isabelle nowadays is Isabelle/HOL, providing a higher-order logic theorem proving environment.
 Isabelle/HOL includes several  specification tools, e.g. for datatypes, inductive definitions and functions with complex pattern matching.
 Proofs are written in the structured proof language Isar. Isabelle implements several tools to increase the user's productivity in theorem proving.
 \begin{figure}[htbp]
 \centering
 %\includegraphics[bb=0 0 10 10]{coqide.png}
-\includegraphics[scale=0.25]{coqide.png}
+\includegraphics[scale=0.25]{fig/coqide}
 \caption{CoqIDE main screen}
 \end{figure}
 (http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
 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
 and it's easy to add to your own theories.
 (http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME)
 \begin{figure}[htbp]
 \centering
-\includegraphics[scale=0.5]{pgisabelle.png}
+\includegraphics[scale=0.5]{fig/pgisabelle}
 \caption{Proof General for Isabelle}%
 \end{figure}
 \subsubsection{Isabelle/Jedit}
 jEdit is a text editor for programmers, written in Java.
 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much
 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, 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. \\
 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.\\
 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.\\
-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.  \\
+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.
-The main reasons are:\\
+The main reasons are:
 \begin{enumerate}
-\item quick exhaustion of virtual address space\\
+\item quick exhaustion of virtual address space
-\item locking mechanisms often lack suitable contention managers\\
+\item locking mechanisms often lack suitable contention managers
 \end{enumerate}
 %[IoC]
-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.\\
+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.
-Concurrent processes are usually implemented by using a thread-based or an event-based strategy. 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.\\
+\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.
-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].
-Supports blocking operations and can be executed on multicore processors in parallel.\\
+\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].
-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.\\
+Supports blocking operations and can be executed on multicore processors in parallel.
-The implementation of 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. \\
-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.\\
+\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.
+\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.
+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.
 receive:         def receive[R](f: PartialFunction[Any, R]): R
 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]. \\
-react:          def react(f: PartialFunction[Any, Unit]): Nothing
+react:
+$$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
 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]. \\
 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. \\
 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.\\
 Event-Based Programming without Inversion of Control - Philipp Haller, Martin Odersky  [IoC]\\
 Scala actors: Unifying thread-based and event-based programming - Philipp Haller, Martin Odersky [2.P]\\
 This plan involves the following details.
 \subsection{Add a plug-in to jEdit}\label{plugin}
 % file structure, copied from example project ...
 %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?\\
-jEdit 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. \\\\
+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. \\\\
 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.\\
 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.
 To get more information about the jEdit infrastructure see: http://jedit.org/users-guide/plugin-intro
 \\\\
 %isabell plugin beschreiben!!!!!!!!

branch	decompose-isar
changeset 38091	a1cc2a17498b
parent 38090	4e128838c313
child 38092	4860796a7f7d
child 38093	ec4b1dfb6807
child 38098	35218563ed7b
child 38103	a5ca97e593f6