| Line 20: | Line 20: | ||
== Explanation of the basic programmatic abstractions == | == Explanation of the basic programmatic abstractions == | ||
The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, History, and StateSpace abstractions. The Model provides all the static information about the model that is currently being checked or animated. The StateSpace provides the corresponding label transition system for the Model. The History corresponds to exactly one trace throughout the StateSpace. A more detailed description of the different is available in the [[Programmatic Abstractions in the ProB 2.0 API]]. | |||
== Tutorial of the Current Features of ProB 2.0 == | == Tutorial of the Current Features of ProB 2.0 == | ||
Something. | Something. | ||
One of the main goals that we wanted to build our UI on top of a programmatic API. Our goal was to bring the ProB 2.0 API into a scripting language and not to bring the scripting language into the API.
We also attempted to apply functional programming techniques to our project wherever it was possible. This included trying to create small abstractions that could be composed in different ways. For example, we tried to avoid very large interfaces, but instead preferred to have small functions and methods that accomplish one single task. For this same reason, we tried to use immutable data structures wherever possible.
The ProB API needs to deal with many different formalisms (i.e. Classical B, Event B, Z, CSP, etc.). For this reason, we constucted our data structures so that they can be easily adapted for other formalisms.
While developing a particular feature, it is very helpful to be able to easily experiment and interact with the tool. For this reason, we have spent quite a bit of energy developing a developer friendly console for testing out features as they are being developed.
The scripting language that we chose is Groovy. It is a dynamically typed JVM language. Because of the seamless integration between Java and Groovy libraries, we can easily integrate any jar library into the ProB API, and the code that we produce can also be fully integrated into any other Java project.
Groovy also has many features that make it an ideal scripting language. It provides closures which allow the definition of higher order functions. It is also possible to perform meta programming and thereby redefine or modify existing groovy or java class files. For example, in ProB 2.0, we redefined the java.lang.String class so that we can specify the correct Parser with which a string should be parsed.
The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, History, and StateSpace abstractions. The Model provides all the static information about the model that is currently being checked or animated. The StateSpace provides the corresponding label transition system for the Model. The History corresponds to exactly one trace throughout the StateSpace. A more detailed description of the different is available in the Programmatic Abstractions in the ProB 2.0 API.
Something.