Testing Installation of SPARK Ada (Gnatstudio) on Linux Machines in the Linux Lab

Preliminaries

• In the following we use the Linux terminology "directory" for what is called in Windows "folder".
• The example code for testing SPARK Ada is an adaption of the code from the lecture sect6/example6-19.
• Download the git repository following the instructions for downloading the git repository
• The example code for testing can be found in the subdirectory exampleCodeForTestingInstallations
  • Direct link in git repository

Testing Installation of SPARK Ada (Gnatstudio)

• Now open the file browser (dolphin) which is on the start menu.
• Navigate to exampleCodeForTestingInstallations
• If you click on the file main.gpr (NOT main.adb or main.ads) Gnatstudio should start.
  This might take a while initially because it initialises some data when used the first time.
• It should look approximately like the following Screenshot
• If it opens instead in an editor (usually kate) you need to manually associate the filextension with the application
  • Right click on main.gpr, choose "open with"
  • Search for callgps
  • Don't tick "open with Konsole"
  • Tick to remember the selection.
  • Do the same below in section "Testing installtion of why3" for a file with extension .mlw, associate it with "callwhy3".
• Should starting of Gnatstudio fail, Gnatstudio might not be installed on your machine.
  • If in Linux Lab, tell instructors about which machine has the problem (need to look at the machine name on a konsole prompt) so that system adminstrators can fix it later.
  • Go to a different machine.
• If you haven't installed SPARK Ada and Why3 using script (e.g. on your own computer), you can
  • Either manually associate the extension .gpr with the command callgps and the extension .mlw with the command callwhy3
  • or start those commands from a console, calling
    callgps main.gpr
    or
    callwhy3 file.mlw
    where file.mlw is a mlw file you want to see in why3.

Basic Usage of Gnatstudio

Testing Installation of Why3 (Optional)

• Why3 is currently not installed in the Linux Lab and not required for the labs, the following is only useful if you want to install why3 on your own Linux computer (not really needed).
• Navigate (in dolphin) to the subdirectory gnatprove
• Click on the file main.mlw
• why3 should start.
  • If it doesn't start why3 might not be installed.
  • If in Linux Lab, tell instructors about which machine has the problem (need to look at the machine name on a konsole prompt) so that system adminstrators can fix it later.
  • Go to a different machine.
• Currently why3 will display an error message as in this Screenshot.
  • You can ignore this message (which is due to different libraries used by SPARK Ada and why3).
  • Please press the "close" button.
• The main window should look approximately look like the following Screenshot.
• Close why3, we won't need it at the moment. We only tried it out to test the installation.