Introduction to SPARK 2014
How to Develop Ultra-Low Defect Software
This tutorial aims at giving a practical, hands-on introduction to SPARK 2014, a modern, imperative and object-oriented programming language, specifically conceived for the development and formal verification of high-integrity software. We cover basic features of the language, such as data types, concurrency and contracts, and then apply static verification to prove the correctness of contracts, as well as the absence of run-time errors (such as overflows, division by zero or even race conditions). Further topics include the inclusion of legacy code, the combination of testing and static analysis, the precision of numerical operations, and a brief outlook on secure programming for data-sensitive applications. We close the tutorial with an example of how these tools can be used in a practical setting.
Please install the GPL version of GNAT and SPARK 2014 before the tutorial. Installation hints are given in the following.
- Visit www.libre.adacore.com
- Click on GNAT GPL 2017
- Select "Free Software or Academic Development"
- optionally provide email address
- click on "Build Your Download Package"
- From dropdown, select the correct platform for your machine, e.g., x86 Windows (32bits) for a Windows Laptop (Note: 32bits will also work on 64bit Windows)
- Expand and select nodes GNAT Ada 2017 and SPARK Discovery 2017
- Click on "Download Selected Files" and wait for completion.
- unpack the zip file in your downloads folder. A new folder with your <platform> appears (e.g., x86_64-linux, x86-windows, etc.)
- Linux users only: unpack the two tar.gz files within the subfolders of the <platform> folder
- execute the installation program within subfolder x86-windows/adagpl-2017/gnatgpl
- execute the installation program within subfolder x86-windows/adagpl-2017/spark2014-discovery
- Open a terminal, navigate to the subfolder <platform>/adagpl-2017/gnatgpl/gnat-gpl-<platform>
- run doinstall.sh. The script will ask for a location to install the tools. Leave defaults if you have no preferences.
- At the end of the script, you will see a message like follows:
To use SPARK 2014, users must put /tmp/gnat/bin in front of their PATH environment variable. The following commands enable you to do this: PATH=/tmp/gnat/bin:$PATH # Bourne shell setenv PATH /tmp/gnat/bin:$PATH # C shell Thank you for installing SPARK 2014!
Follows the instructions on your screen. If you want to make this setting permanent, consider extending your path variable in the ~/.bashrc or ~/.profile file (making these settings not permanent, means that the tools will only work on this very terminal, or if you set the PATH variable again in a new terminal).
- Repeat the same process for the subfolder <platform>/adagpl-2017</platform>/spark2014-discovery/spark-discovery-gpl-2017-<platform>-bin
- Keep this very terminal opened, unless you have made your settings permanent.
4. Test your Installation
Please do test your installation! Missing path variables or wrongly chosen configurations may otherwise stop you from following this tutorial.
- Start the Integrated Development Environment (IDE) "GPS"
- Windows: Find GNAT/GPS in the Start Menu and click to open
- Linux: open a terminal (or use the same you used for installation) and type "gps"
- If that command is not recognized, make sure that you have your PATH variable set correctly (see installation), otherwise try installing again while making sure that you have the right version for your platform.
- Click on "Create New Project"
- Select "Basic -> Simple Project", click "Next", then "Apply". The IDE opens.
- At the left side, expand folder "src" and open file "main.adb" by double clicking.
- Replace the file content with the following:
procedure Main with SPARK_Mode is n : Natural; begin n := n + 1; end Main;
- First, we check whether the compiler is working:
- Click the menu "Build > Project > Build & Run > main.adb". The messages window (tab at the bottom) should end with "process terminated successfully".
- If that is not the case, please re-install GNAT, making sure that you have the right version for your platform.
- Next, we check whether the SPARK tools are working:
- Click the menu "SPARK > Prove All Sources". A window opens.
- Click on "Execute". The messages window should contain something like "main.adb:4:11: medium: overflow check might fail".
- If that is not the case, please re-install SPARK 2014, making sure that you have the right version for your platform and that the PATH variable also points to the install location.
- If you are lacking the entire SPARK menu in the toolbar, see previous step.
- If you passed the previous two steps, then you are ready to develop programs in SPARK 2014, congratulations!
- Tutorial Slides (updated 14-Sep-2017)
- Source Codes from this Tutorial:
- SPARK Mini Cheat Sheet at github
- Another SPARK tutorial (linear search, bit more complex): in the SPARK User Guide
- Since SPARK is a subset of Ada: