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 will probably NOT be required for lab tasks in the labs 2022/23, but we might 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 here
• Back to main page for SPARK Ada related to CSCM13/CSC313