Rodin Handbook





 

3.1.1 Eclipse in General

From the Eclipse Website1: Eclipse is an open source community, whose projects are focused on building an open development platform comprised of extensible frameworks, tools and runtimes for building, deploying and managing software across the lifecycle. The Eclipse Foundation is a not-for-profit, member supported corporation that hosts the Eclipse projects and helps cultivate both an open source community and an ecosystem of complementary products and services.

From Wikipedia2: Eclipse is a multi-language software development environment comprising an integrated development environment (IDE) and an extensible plugin system. It is written mostly in Java and can be used to develop applications in Java and, by means of various plugins, other programming languages including Ada, C, C++, COBOL, Perl, PHP, Python, R, Ruby (including Ruby on Rails framework), Scala, Clojure, Groovy and Scheme. It can also be used to develop packages for the software Mathematica. The IDE is often called Eclipse ADT (Ada Development Toolkit) for Ada, Eclipse CDT for C/C++, Eclipse JDT for Java, and Eclipse PDT for PHP.

Eclipse provides the technical foundation of Rodin.

3.1.1.1 Project Constituents and Relationships

The primary concept in doing formal developments with the Rodin Platform is that of a project. A project contains the complete mathematical development of a Discrete Transition System. It consists of components of two different types: machines and contexts. Machines contain the variables, invariants, theorems, and events for a project. Contexts contain the carrier sets, constants, axioms, and theorems for a project. Figure 3.1 shows an overview.

Machine
  • variables

  • invariants

  • events

Context
  • carrier sets

  • constants

  • axioms

Figure 3.1: Overview Machine and Context

Various relationships exist between machines and contexts. This is illustrated in the following figure. A machine can be “refined" by another one, and a context can be “extended" by another one. However, cycles are not allowed (i.e. the original machine cannot refine any of the refined machines). A machine can also “see" one or several contexts. A typical example of machine and context relationship is shown in Figure 3.2.

\includegraphics[width=0.5\textwidth ]{img/reference/ref_10_project2.png}
Figure 3.2: A typical example of machine and context relationship

3.1.1.2 Rodin Nature

Eclipse Projects can have one or more natures to describe their purpose. The GUI then adapt to this nature. Rodin Projects must have the Rodin-Nature. If you create an Event-B project in Rodin, it automatically has the right nature. If you want to modify an existing project, you can edit the .project file and add the following XML in the <natures> section:

\includegraphics[width=7mm]{img/pencil_64.png}

<nature>org.rodinp.core.rodinnature</nature>