Eiffel Verification Environment

Contents

Introduction

The goal of this project is to unify all the efforts that aim at adding new, experimental functionalities to Eiffelstudio. All the additional tools will then merge into a single research branch of EiffelStudio, code-named Eve (Eiffel Verification Environment). The tool includes the outgrowth of AutoTest, Eve Proofs, CDD, Ebbro, Escher, Origo plugin, Proof-Transforming Compilation, SCOOP, and anything else we may dream of in the future. As soon as the various tools prove their usefulness they will be integrated into the main EiffelStudio release.

Participation

If you want to join this project, please write an email to Yi Wei at yi.wei@inf.ethz.ch containing your Origo user name.

Subversion

Important: Before you check out the source code, following the instructions at [4] to setup subversion.

Note: Only use this Eve project to create Wikis, forums and issues. Don't use this Eve project subversion URLs from the Development page. In fact, we decided to use the repository of the EiffelStudio project because Eve project indeed is a branch from the EiffelStudio project repository. Therefore, developers should always use the EiffelStudio project repository. To be able to commit code to the EiffelStudio project, developers need to join it.

Compiling EVE

On Windows

Software Installation

1. Install VisualStudio 2008 from ides: [5]

2. Install EiffelStudio from Sourceforge: [6]

  Alternatively, you can use a script [7] to download and install the latest EiffelStudio release. 
  In order to use this script, you need to have python.exe and 7z.exe in your PATH.
  The easiest way to use the script is: go to the directory where you want to put your EiffelStudio release, 
  then type "python install_es.py".

Environment variable setup

1. ISE_EIFFEL - the directory of EiffelStudio release

2. EIFFEL_SRC - the directory of EiffelStudio source code

3. ISE_PLATFORM - the value is windows on a 32bit machine and win64 on a 64bit machine.

4. ISE_LIBRARY - the value is %EIFFEL_SRC%

5. ISE_C_COMPILER - the value is msc

6. Put %ISE_EIFFEL%\studio\spec\%ISE_PLATFORM%\bin into you %PATH%

7. Goto VisualStudio 2008 Command Prompt, get the values of environment variables LIB, INCLUDE (use "echo %LIB%"), declare these two variables in your own setting with the given values.

8. Goto VisualStudio 2008 Command Prompt, get the value of environment variables %PATH%, copy VisualStudio related part into your own %PATH%. For example, on my machine, VisualStudio 2008 is installed at c:\apps\vc9, so the VisualStudio related part in my %PATH% is:

C:\apps\vs9\VC\BIN\amd64;C:\Windows\Microsoft.NET\Framework64\v3.5;C:\Windows\Microsoft.NET\Framework64\v3.5\Microsoft .NET Framework 3.5 (Pre-Release Version);C:\Windows\Microsoft.NET\Framework64\v2.0.50727;C:\apps\vs9\VC\VCPackages;C:\apps\vs9\Common7\IDE;C:\apps\vs9\Common7\Tools;C:\apps\vs9\Common7\Tools\bin;C:\Program Files\\Microsoft SDKs\Windows\v6.0A\bin\x64;C:\Program Files\\Microsoft SDKs\Windows\v6.0A\bin\win64\x64;C:\Program Files\\Microsoft SDKs\Windows\v6.0A\bin;

9. Follow the instructions at: [8] to setup subversion config file.

Compiling EVE source

1. Check out source code from [9] into EIFFEL_SRC

2. Check out scripts to compile run-time and C libraries from [10]

3. Start a console, run compile_ec_win32.bat or compile_ec_win64.bat depending on your platform, and then run copy_run_time.bat.

4. Start EiffelStudio, open the ec.ecf file at %EIFFEL_SRC%\Eiffel\Ace, and choose the "bench" target.

On Linux

Software Installation

1. Install EiffelStudio from Sourceforge: [11]

  Alternatively, you can use a script [12] to download and install the latest EiffelStudio release.
  The easiest way to use the script is: 
  then type python install_es.py --install-dir <directory>, where <directory> is the place you want to put EiffelStudio.

Environment variable setup

1. ISE_EIFFEL - the directory of EiffelStudio release

2. EIFFEL_SRC - the directory of EiffelStudio source code

3. ISE_PLATFORM - the value is linux-x86 on a 32bit machine and linux-x86-64 on a 64bit machine.

4. ISE_LIBRARY - the value is $EIFFEL_SRC

6. Put $ISE_EIFFEL/studio/spec/$ISE_PLATFORM/bin into you %PATH

7. Follow the instructions at: [13] to setup subversion config file.


Compiling EVE source

1. Check out source code from [14] into EIFFEL_SRC

2. Check out scripts to compile run-time and C libraries from [15]

3. Install the packages "libgtk2.0-dev" and "libxtst-dev"

4. Start a console, run compile_runtime.sh.

5. Start EiffelStudio, open the ec.ecf file at $EIFFEL_SRC/Eiffel/Ace, and choose the "bench" target.

   Alternatively, to do steps 4 and 5, you can run the compile_ec.py script from [16]. 
   The easiest way to use it is to type python compile_ec.py.
   After the script terminates, workbench will be compiled in $EIFFEL_SRC/Eiffel/Ace/EIFGENs.


On Mac OS X

Software Installation

  1. Install MacPorts by following the instructions on the project's page.
  2. Install EiffelStudio from MacPorts.
    1. Open the Terminal application on your operating system (normally found under /Applications/Utilities/) and type port search eiffelstudio to list all available ported EiffelStudio releases.
    2. Choose a release, e.g. eiffelstudio68 and install it with the command sudo port install eiffelstudio68. Because EiffelStudio is built from source, this might take a long time, if you're using an older machine.

Software Installation by Customizing Portfile

It might happen that the EiffelStudio port in MacPorts is not up-to-date with the latest EiffelStudio builds. In that case you have the option to manually modify the port file for EiffelStudio yourself to still get the latest version compiled and installed.

  1. Open http://sourceforge.net/projects/eiffelstudio/files/, select the subfolder for the corresponding EiffelStudio release, e.g. "EiffelStudio 6.8", and inside the subfolder for the build version you want to install, e.g. "Build_86627".
  2. Download the Porter Package file, e.g. "PorterPackage_68_86627_gpl.tar", to a local folder. The instructions below will be based on this file name as a given example.
  3. Open the Terminal application and navigate to the folder where you stored the Porter Package. Run the following command (see the first box) to get the hash of the Porter Package (see second box) that you'll need to update the Portfile later on:

  1. openssl dgst -ripemd160 PorterPackage_68_86627_gpl.tar
  1. RIPEMD160(PorterPackage_68_86627_gpl.tar)= ff763bb7091fc37a236dda0589d7fbde22750fe4

Updating the Portfile

Open the Terminal application and run command below to open the Portfile for the corresponding EiffelStudio release in a text editor. Afterwards you can continue to update the fields.

  1. open -a TextEdit /opt/local/var/macports/sources/rsync.macports.org/release/ports/lang/eiffelstudio68/Portfile

Ensure that the "minor version" field, i.e. the built version, is set correctly, e.g.:

  1. name              eiffelstudio68
  2. set minor_version 86627
  3. version           6.8.${minor_version}

Ensure that the "distname" field reflects the Porter Package filename, e.g.:

  1. distname          PorterPackage_${branch}_${minor_version}_gpl

Ensure that the "checksums" section contains the right checksum for the downloaded Porter Package file, e.g.:

  1. checksums         ${distname}${extract.suffix} rmd160 ff763bb7091fc37a236dda0589d7fbde22750fe4 \

Environment (variable) setup

To achieve a consistent setup for bash and X11, we recommend to edit following files located in your home directory: .bashrc, .bash_profile and .profile. if the files don't exist, you'll have to create them. If they exist and already have content, add the given lines just anywhere.

Edit file $HOME/.bashrc

A successful installation of eiffelstudio will print out at the end instructions like the following example:

  1. export ISE_PLATFORM=macosx-x86-64
  2. export ISE_EIFFEL=/Applications/MacPorts/Eiffel68
  3. export GOBO=$ISE_EIFFEL/library/gobo/svn
  4. export PATH=$PATH:$ISE_EIFFEL/studio/spec/$ISE_PLATFORM/bin:$GOBO/../spec/$ISE_PLATFORM/bin
Copy your individual output to .bashrc or modify the above given example to your needs. Further add following two lines to the previous configuration and take care to set EIFFEL_SRC to a directory that will contain the source of the EVE branch.
  1. export EIFFEL_SRC=/Dummy/Path/To/My/Source
  2. export ISE_LIBRARY=$EIFFEL_SRC

Edit file $HOME/.bash_profile

The beginning of this file should link to the .bashrc that we previously set up:

  1. . ~/.bashrc
  2. ENV=$HOME/.bashrc
  3. export ENV

Edit file $HOME/.profile

The beginning of this file should link to the .bash_profile that we previously set up. This step is necessary to propagate the environmental settings to the X11 X window system:

  1. . ~/.bash_profile

Configuration of Subversion

Please, follow the instructions at [17] to setup the Subversion configuration file.

User interface tweaking

Optional, but highly recommended: If you'd start EiffelStudio now, you'd get a very disappointing visual experience. With the installation of additional themes you can reduce that impact.

  1. Execute the command port install gnome-themes gtk-theme-switch to install additional themes and an application that allows to switch between them.
  2. After installation execute switch2 in Terminal, which opens a simple theme switching application. Select (if not already done) Clearlooks or any other theme that is appealing to you.

Compiling EVE source

  1. Check out source code from [18] into EIFFEL_SRC
  2. Check out scripts to compile run-time and C libraries from [19]
  3. Start a console, run compile_runtime.sh.
  4. Start EiffelStudio, open the ec.ecf file at $EIFFEL_SRC/Eiffel/Ace, and choose the "bench_unix" (or "bench") target.
   Alternatively, to do steps 3 and 4, you can run the compile_ec.py script from [20]. 
   The easiest way to use it is to type python compile_ec.py.
   After the script terminates, workbench will be compiled in $EIFFEL_SRC/Eiffel/Ace/EIFGENs.

Working Guidelines

Subversion Branching and Merging

When you do branching, you need to contain the following text at the beginning of your commit message:

<<Branched from URL at rev#N>>

When you do merging, you need to contain the following text at the beginning of your commit message:

<<Merged from URL at rev#N>>

The URL is the source of branch or merging. You don't need to include the complete URL because that would be quite heavy. You can use a relative path starting from the root of the repository instead.

The N in rev#N is the revision number of the branch. For example, if you branched from the Eve project code base at revision 12345, then you need to include the following message:

<<Branched from /branches/eth/eve at rev#12345>>

Code Style Guidelines

[21]


Release Plan

More recent releases

Since May 2010, the EVE project is synchronized with EiffelStudio trunk every week. So checkout the source code of eve will give you the most updated revision.

Eve 6.3

The release date is April 30th 2009. This release will be based on EiffelStudio 6.3 release and will have the following tools integrated:

  • AutoTest
  • Contract Driven Development (CDD)
  • Eiffel Object Browser (Ebbro)
  • Eiffel Schema Evolution Support (Escher)
  • Proof-Transforming Compilation

Download You can download Eve 6.3 at: [22].

Release Notes For the moment, only Windows platform is supported and Microsoft C compiler is needed. Check here for information about how to install Microsoft C compiler.

Installation Unzip the file and set the following environment variables:

  • ISE_EIFFEL = the unzipped directory, for example c:\eve63.
  • ISE_LIBRARY = %ISE_EIFFEL%
  • ISE_C_COMPILER = msc
  • ISE_PLATFORM = windows
  • Add %ISE_EIFFEL%\studio\spec\%ISE_PLATFORM%\bin into your %PATH% variable.

Running The Eve 6.3 executable is %ISE_EIFFEL%\studio\spec\%ISE_PLATFORM%\bin\estudio.exe.

Documentation You can find more info about the single projects in the docs page.