
diff -r 4872b10c8747 -r 90c4c3bb47d9 doc-src/isac/CTP-userinterfaces.tex
--- a/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 08:03:23 2011 +0100
+++ b/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 08:10:06 2011 +0100
@@ -56,35 +56,32 @@
 %\cite{pl:milner97}
 %for developing CTP
 \subsubsection{Standard ML}
-Standard ML is a general-purpose, modular, functional programming language. 
+Standard ML is a general-purpose, modular, functional programming language. \cite{pl:milner97}
 Programs written in Standard ML consist of expressions to be evaluated, as opposed to statements or commands. 
-SML is a modern descendant of the ML programming language used in the Logic for Computable Functions (LCF) theorem-proving project. 
-It is invented by Robin Milner. %http://en.wikipedia.org/wiki/Standard_M 
+Functional programming languages constitude a ???? very differnt of object orientated languages, see Sect. \ref{ml-users}. ML originated from the LCF-project(Logic for Computable Functions)\cite{meta-Ml}, where it had been developed as a meta language. Since ML has been standardised this family of language is called Standard ML. Important for the logical foundation of SML is the $\lambda$-calculus.
+%http://en.wikipedia.org/wiki/Standard_M 
 \subsubsection{Coq}
-Coq is an interactive theorem prover, developed in France. The team leader is Senior Scientist Benjamin Werner. 
-Coq is in Objective Caml programmed, an ML based programming language.
-It has the ability to express  mathematical  assertions and check proof of mathematical  assertions. 
+Coq is an interactive theorem prover, developed in France.
+It is programmed in Objective Caml, an ML based programming language.
+It has the ability to express  mathematical  assertions and check proof of mathematical assertions. 
 Furthermore Coq includes automatic theorem proving tactics and decision procedures.
-Proof development in Coq is done through a language of tactics that allows a user-guided proof process. 
-At the end, the user can check that tactics build lambda-terms. 
+Properties, programs and proofs are written a functional programming language called the Calculus of Inductive Constructions (CIC).
+Proof development in Coq is done through a language of tactics that allows a user-guided proof process.\cite{coq1999}
+  
 Another feature of Coq is “that it can automatically extract executable programs from specifications, as either Objective Caml 
 or Haskell source code.“
-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)
+
+There are many easy-to-read introductions to Coq \footnote{http://coq.inria.fr/a-short-introduction-to-coq} on the internet.
 \subsubsection{Isabelle}
 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 is developed at University of Cambridge (Larry Paulson), Technische Universit\"at M\"unchen
+and Université Paris-Sud. Isabelle is called a framework, because it implements serveral object logics.
+The most widespread logic of Isabelle is Isabelle/HOL, short for higher-order logic.
 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. 
-Isabelle's classical reasoner is used to check formulas. The simplifier can reason with and about equations. 
-Linear arithmetic facts are proved automatically.
+Proofs are written in the structured proof language Isar.\cite{wenzel:isar} Isabelle implements several tools, e.g. a reasoner, a simplifier and powerful automatic provers(Slegehammer), increase the user's productivity in theorem proving. 
 Isabelle provides notational support: new notations can be introduced, using normal mathematical symbols.
 Definitions and proofs may include LaTeX source, from which Isabelle can automatically generate typeset documents.
-Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell.
+Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell.\cite{Haftmann-Nipkow:2010:code}
 (http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html)
 \subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa}
 %     CoqIDE, ..
@@ -121,7 +118,7 @@
 (http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
 \subsubsection{Proof General for Isabelle}
 Proof General is a generic front-end for proof assistants, based on the customizable text editor Emacs.
-Proof General has been developed at the LFCS in the University of Edinburgh with contributions from other sites.
+It has been developed at  the University of Edinburgh with contributions from other sites.
 Proof General comes ready-to-go for these proof assistants: Isabelle, Coq, PhoX, LEGO.
 Proof General is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. 
 The communication between the user and the theorem prover takes place via two or  more Emacs text widgets. 
@@ -142,13 +139,13 @@
 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much 
 smaller and better focused on its primary task of text editing.
 The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs.
-The main Isabelle/jEdit plugin consists of ≈ 10 small Scala files  that augment some key jEdit components in order to provide a metaphor of asynchronous 
+The main Isabelle/jEdit plugin consists of ten small Scala files  that augment some key jEdit components in order to provide a metaphor of asynchronous 
 proof document editing. 
 Isabelle/jEdit integrates the jEdit 4.3.2 framework  and some further  jEdit plugins. 
 It also implements custom-made IsabelleText Unicode font that actually contains the usual Isabelle symbols that users expect from long 
 years of Proof General X-Symbol support. 
 The editor provides useful feedback, via semantic information from the processed document in the background. 
-This achieves continuous proof checking based on our 
+This achieves continuous proof checking based on 
 asynchronous prover toplevel. A lot of information can be directly attached 
 to the source text, via coloring, tooltips, popups etc.
 
@@ -319,46 +316,39 @@
 \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?\\
-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.
-
-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.
-
+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!!!!!!!!
 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:
 \begin{itemize}
+\item 14 Scala-source-files
+\item three XML-files
 \item one property file
-\item three XML-files
-\item 14 Scala-source-files
 \end{itemize}
 %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. 
-\begin{description}
-\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.
-\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.
-\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.
-\item[services.xml] The last XML-file is \textit{services.xml} and is used to create instances of needed jEdit-Plugins.
-\end{description}
-This four files are located in the folder \textit{plugin}.\\
-
-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: 
-\begin{description}
-\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!
-\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}.
-\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.
-\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.
-\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.
-\end{description}
-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.
-%\begin{itemize}
-%\item $html_panel.scala$
-%\item $isabelle_encoding.scala$
-%\item $isabelle_hyperlinks.scala$
-%\item $isabelle_options.scala$
-%\item $isabelle_token_maker.scala$
-%\item $isabelle_hyperlinks.scala$
-%\end{itemize}
+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. \\
+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.\\
+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.\\
+The last XML-file is \textit{services.xml} and is used to create instances of needed jEdit-Plugins.\\
+This four files are located in the folder \textit{plugin}.\\\\
+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: \\
+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! \\
+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}.\\
+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.\\ 
+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.\\
+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.\\
+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:
+\begin{itemize}
+\item $html_panel.scala$
+\item $isabelle_encoding.scala$
+\item $isabelle_hyperlinks.scala$
+\item $isabelle_options.scala$
+\item $isabelle_token_maker.scala$
+\item $isabelle_hyperlinks.scala$
+\end{itemize}
 
 
 %  Like each other jEdit-Plugin also this 
@@ -367,14 +357,13 @@
 
 \subsection{Details of NetBeans projects}\label{netbeans}
 %     Scala + Java: html project files
-As described in the last paragraph, jEdit is a open-source-project. The jEdit-developers use a NetBeans-project to produce the source-code and so it is beneficial to use a NetBeans project too, because there is a quite good documentation about setting up a NetBeans-project with the jEdit-source.\footnote{See http://wiki.netbeans.org/NetbeansedJEdit for further information.} 
-
+As described in the last paragraph, jEdit is a open-source-project. The jEdit-developers use a NetBeans-project to produce the source-code and so it is beneficial to use a NetBeans project too, because there is a quite good documentation about setting up a NetBeans-project with the jEdit-source. See http://wiki.netbeans.org/NetbeansedJEdit for further information.\\\\
 If you want to set up a new jEdit-Plugin-project you have to attend that you have to create some source-files and that there must be a connection to the jEdit-source because you will need to exchange data with the jEdit engine. This could probably look like: \textit{jEdit.getProperty("options.isabelle.isabelle")}\\
 As shown above, the jEdit-source is needed to compile and build your Plugin. There are two ways to organize your project:
-%\begin{itemize}
-%\item with jEdit source code - two projects in one
-%\item with jedit.jar library
-%\end{itemize}
+\begin{itemize}
+\item with jEdit source code - two projects in one
+\item with jedit.jar library
+\end{itemize}
 \subsubsection{Plugin with jEdit-source}
 It is a good way to download the jEdit source as Netbeans project because then it is possible to add another subproject to the existing jEdit-NetBeans-project. As you see it is also possible to mix Scala and Java. A big advantage is, that debugging will now work really fine. If you want to set up a project like this, you should complete the following steps.
 \begin{enumerate}
@@ -404,21 +393,15 @@
 \end{itemize}
 %* kurze aufzählung der xml-netbeans-files + erklärung\\
 \subsubsection{NetBeans project files}
-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!).
-
-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.
-
+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!).\\
+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.\\
 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.
 
 \subsection{Use interfaces between Java and Scala}\label{java-scala}
 %     how are data exchanged between Scala and Java ...
-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.
-
-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.
-
-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.
-
-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.
+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.\\
+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.\\
+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.\\
 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:
 \begin{enumerate}
 \item \textit{import javax.swing.JButton}
@@ -429,6 +412,9 @@
 \end{enumerate}
 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! 
 %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. ...
+http://www.scala-lang.org/api/current/scala/swing/Button.html\\
+http://download.oracle.com/javase/1.4.2/docs/api/javax/swing/JButton.html
+
 \section{Conclusion and future work}
 
 




