doc-src/isac/CTP-userinterfaces.tex
branchdecompose-isar
changeset 38099 a3cae5ca93eb
parent 38096 4872b10c8747
parent 38098 35218563ed7b
child 38100 905c8bfcf39a
equal deleted inserted replaced
38096:4872b10c8747 38099:a3cae5ca93eb
   169 So it is necessary to use proof documents instead of proof scripts.  
   169 So it is necessary to use proof documents instead of proof scripts.  
   170 Proof scripts are  sequences of commands however proof documents are  structured texts. 
   170 Proof scripts are  sequences of commands however proof documents are  structured texts. 
   171 So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. 
   171 So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. 
   172 (MW async-isabelle-scala.pdf)
   172 (MW async-isabelle-scala.pdf)
   173 \newpage
   173 \newpage
       
   174 
       
   175 
       
   176 
       
   177 
       
   178 
   174 %Andreas
   179 %Andreas
   175 \section{Isabelle's plans for new user-interfaces}\label{gui-plans}
   180 \section{Isabelle's plans for new user-interfaces}\label{gui-plans}
   176 %       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
   181 %       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
   177 %       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
   182 %       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
   178 %
   183 %
   181 %hundreds of proof obligations are generated during a software verification process 
   186 %hundreds of proof obligations are generated during a software verification process 
   182 %
   187 %
   183 %so the final goald of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE).
   188 %so the final goald of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE).
   184 %
   189 %
   185 %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.
   190 %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.
       
   191 The following observations lead to novel requirements for CTPS' userinterface:
   186 
   192 
   187 \begin{itemize}
   193 \begin{itemize}
   188 \item theorem proving will be integrated into software development
   194 \item theorem proving will be integrated into software development
   189 \item hundreds of proof obligations are generated during a software verification process
   195 \item hundreds of proof obligations are generated during a software verification process
   190 \item so the final goal of Isabelle's planning is integration with other software development tolls in an integrated development environment (IDE)
   196 \item so the final goal of Isabelle's planning is integration with other software development tolls in an integrated development environment (IDE)
   191 \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
   197 \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
   192 \item favorite IDE is the jEdit, because it is clearer than Eclipse or NetBeans. The reason behind this choice follows in section 4.2
   198 \item favorite IDE is the jEdit, because it is clearer than Eclipse or NetBeans. The reason behind this choice follows in section \ref{plugin}
   193 \end{itemize}
   199 \end{itemize}
       
   200 
       
   201 These indicate design decisiouns are sketched in the sequel.
   194 
   202 
   195 \subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
   203 \subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
   196 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.
   204 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.
   197 
   205 
   198 
   206 
   219 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.
   227 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.
   220 
   228 
   221 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}.
   229 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}.
   222 
   230 
   223 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.
   231 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.
   224 %
   232 
   225 %\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:
   233 \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:
   226 %
   234 
   227 %TODO
   235 \begin{verbatim}
       
   236    public class Calcstate
       
   237    {
       
   238      private Program program_;
       
   239      private Tree<Step> calcstate_;
       
   240      private Position position_;
       
   241      
       
   242      public Calcstate(Program program) {...}
       
   243      public Step do_next() {...}
       
   244      public List<Step> apply_tactic(Tactic tactic) {...}
       
   245      public List<Step> apply_formular(Formular formular) {...}
       
   246    }
       
   247 \end{verbatim}
   228 
   248 
   229 \subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
   249 \subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
   230 {\em new} %language --- what for, ideas ...
   250 Scala\cite{TODO} 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.
   231 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.\\
   251 
   232 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. \\
   252 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\cite{[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.
   233 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. \\
   253 
       
   254 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\cite{[wiki-11-1s]}. Furthermore Scala supports higher-order functions, currying and allows functions to be nested.
       
   255 
   234 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:
   256 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:
   235 \\
   257 
   236 \begin{itemize}
   258 \begin{itemize}
   237 \item generic classes
   259 \item generic classes
   238 \item variance annotations
   260 \item variance annotations
   239 \item upper and lower type bounds
   261 \item upper and lower type bounds
   240 \item classes and abstract types as object members
   262 \item classes and abstract types as object members
   241 \item compound types
   263 \item compound types
   242 \item explicitly typed self references
   264 \item explicitly typed self references
   243 \item views
   265 \item views
   244 \item polymorphic methods
   266 \item polymorphic methods
   245 \end{itemize}
   267 \end{itemize}
   246 Static types need no explicit declaration but can be given to give the code some clarity.\\\\
   268 
   247 Scala supports threads, but the Scala library contains an actor model inspired from Erlang. Concurrency and Scala actors follow in the next section.\\
   269 Static types need no explicit declaration but can be given to give the code some clarity.
       
   270 
       
   271 Scala supports threads, but the Scala library contains an actor model\cite{TODO} inspired from Erlang\cite{TODO}. Concurrency and Scala actors follow in the next section.
   248 
   272 
   249 %quellen
   273 %quellen
   250 %%http://de.wikipedia.org/wiki/Scala_%28Programmiersprache%29
   274 %%http://de.wikipedia.org/wiki/Scala_%28Programmiersprache%29
   251 %%http://en.wikipedia.org/wiki/Scala_%28programming_language%29
   275 %%http://en.wikipedia.org/wiki/Scala_%28programming_language%29
   252 %%http://creativekarma.com/ee.php/weblog/comments/why_scala_instead_of_java/
   276 %%http://creativekarma.com/ee.php/weblog/comments/why_scala_instead_of_java/
   253 %%http://www.scalasolutions.com/scala
   277 %%http://www.scalasolutions.com/scala
   254 
   278 
   255 
   279 
   256 \subsection{Support for parallel processing}\label{actors}
   280 \subsection{Support for parallel processing}\label{actors}
   257 %actors copied from erlang
   281 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.
   258 
   282 
   259 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. \\
   283 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 these are based on the actor model.
   260 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. \\
   284 
   261 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.\\
   285 %Most of the message passing systems, which are used in practice, are based on the actor model.
   262 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.\\
   286 
   263 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.
   287 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. 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.
       
   288 
       
   289 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{[IoC]}. These systems use a very popular lightweight implementation and a large number of concurrent processes, which can active simultaneously.
       
   290 
       
   291 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.
   264 The main reasons are:
   292 The main reasons are:
   265 \begin{enumerate}
   293 \begin{enumerate}
   266 \item quick exhaustion of virtual address space
   294 \item quick exhaustion of virtual address space
   267 \item locking mechanisms often lack suitable contention managers
   295 \item locking mechanisms often lack suitable contention managers
   268 \end{enumerate}
   296 \end{enumerate}
   269 %[IoC]
   297 \cite{[IoC]}\\
   270 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.
   298 For that reasons Erlang uses lightweight concurrent processes by its own run time system and not by the underlying operating system \cite{[IoC]} and the computations on these platforms are often modeled in an event-driven style, which is complicated and error-prone.
   271 \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.
   299 \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 
   300 
   273 \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].
   301 \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{[2.P]}.
   274 Supports blocking operations and can be executed on multicore processors in parallel.
   302 Supports blocking operations and can be executed on multicore processors in parallel.
   275 
   303 
   276 \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.
   304 \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{[2.P]}. Targets to a large number of actor which can be active simultaneously, because they are more lightweight.
   277 
   305 
   278 \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.
   306 \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.
   279 
   307 
   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.
   308 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{[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 
   309 
   282 receive:         def receive[R](f: PartialFunction[Any, R]): R
   310 \subparagraph{receive:}
   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]. \\
   311 $$\mathit{def}\;\mathit{receive}\mathit{[R]}(f: \mathit{PartialFunction}[Any, R]): \mathit{R}$$
   284 react:          
   312 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 \cite{[2.P]}.
       
   313 \subparagraph{react:}
   285 $$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
   314 $$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
   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]. \\
   315 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 \cite{[2.P]}. 
   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. \\
   316 
   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.\\
   317 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.
   289 Event-Based Programming without Inversion of Control - Philipp Haller, Martin Odersky  [IoC]\\
   318 
   290 Scala actors: Unifying thread-based and event-based programming - Philipp Haller, Martin Odersky [2.P]\\
   319 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.
       
   320 
       
   321 %Event-Based Programming without Inversion of Control - Philipp Haller, Martin Odersky  [IoC]
       
   322 %Scala actors: Unifying thread-based and event-based programming - Philipp Haller, Martin Odersky [2.P]
   291 
   323 
   292 
   324 
   293 % Marco
   325 % Marco
   294 \section{Planned contributions at TU Graz}
   326 \section{Planned contributions at TU Graz}
   295 
   327