Installation of SPARK Ada on Your Own Computer
- For Windows Machines see instructions on Canvas.
- For access to Linux machines you may
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
- We are using in the Linux Lab the latest version (2021).
- The coursework needs to compile and be checked with the 2021 version.
- If there is no menu for choosing a platform and version go to end
where says "More packages, platforms, versions and sources".
- 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).
- Why3 is not required for lab tasks in the labs 2021/22,
but we will demonstrate its usage during the labs.
- 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