Installation of SPARK Ada on Your Own Computer
- Because of limited resources Anton Setzer will only provide support
for using SPARK Ada and Why3 in the Linux Lab.
- Consider as well remote access to
the Linux Lab
- There exist a free version of SPARK Ada, which can be installed under Linux, Windows, Mac
(you can even install some components under LEGO mindstorms, Raspberry Pi,
AVR, and more).
- SPARK Ada is available from Ada Core Libre
(or better go directly to Download page)
- We are using in the Linux Lab the 2015 version, please install this version for your machine in order to be
compatible with the version used in CSCM13/CSC313.
- The coursework needs to compile and be checked with the 2015 version.
- If there is no menu for choosing a platform and version go to end
where says "More packages, platforms, versions and sources".
- You need to install GNAT GPL Ada and SPARK GPL (if you can't find
those you have probably chosen the wrong version, choose 2015 version).
- Installation is relatively easy, just follow the instructions
in the README.txt file.
- Follow the Instructions
for testing SPARK Ada Installation
- Academic version of SPARK Ada
(needs registration, for academics only; apparently the code is the same as the GPL
version, but there is additional support).
- You will not obtain the GUI of the why3 system from SPARK Ada
- The only instructions for installing why3 we are aware of are for Linux,
although we have managed with some effort
to install it on macs
- See some rudimentary Instructions how to install Why3
- Why3 is used only occasionally to display verification conditions,
most work is done using SPARK Ada.
- Therefore the recommendation is to not install it on your own
computer and use the lab for this.
- Since installation is complex Anton Setzer will not
help you with installation of why3 - use the machines in the
Linux Lab for why3.
- Some older instructions (referring to 2014 version) can be found
- Back to main page for SPARK Ada related to CSCM13/CSC313