Lab Sessions Critical Systems CSCM13/High Integrity Systems CSC313

Instructions for Linux Machines

• Download the git responsiory as described in instructions for downloading the gt Repository for CSC313/CSCM13
• Now we want to explore some examples.
  • It is important to leave the git repository untouched. Then you can update it by running
    git pull
    rather than having to download the whole repository again and again.
• We first work on the example code for testing the installation.
  • It is located at
    ~/git/criticalhighintegritysystems/exampleCodeForTesting/
    This code is mainly used to check whether everything is set up correctly
    
  • Copy that folder to a location in your file system where you want to work on it (outside the git repository)
  • Now you can follow the Instructions so that you can use SPARK Ada (and why3) from the File Manager
  • Once you have done so, study basic usage instructions of SPARK Ada
  • Now you can look at Examples for getting started
  • Check out SPARK Ada code examples (including Examples from the lectures and other sources)
    
  • The lab sheet and the coursework can be found under Canvas.
    
  • Additional information
    • Cheat Sheet by Olga Petrovska
    • Some basic instructions about using Linux and Emacs can be found here
    • Instructions for setting up machines in the Linux Lab for using SPARK Ada and why3 from command line

Quick Start Guide for Windows Machines

• Follow instructions on Canvas for installing SPARK Ada on your own machine and accessing SPARK Ada on Swanse University computers.
• Then follow the Instructions for Downloading the Git Repository for CSC313/CSCM13 (this may have happened already if you followed the Video guide)
• Test your setup by using the exampleCodeForTesting the installation found in the git repository your installation
• Once you have done so, study basic usage instructions of SPARK Ada
• Now you can look at Examples for getting started
• Check out SPARK Ada code examples (including Examples from the lectures and other sources)
  
• The lab sheet and the coursework can be found under Canvas.
• Cheat Sheet by Olga Petrovska

More extensive instructions

• Test your setup by using Example code for testing your installation
• Check out SPARK Ada code examples (including Examples from the lectures and other sources) The git repository should be uploaded to your computer already.
• Basic Usage Instructions for SPARK Ada
• The lab sheet and the coursework can be found under Canvas.
• It is recommended to first investigate one or more examples of SPARK Ada from the lecture and experiment with them.
• You might try out as well the page on Getting started with SPARK 2014 and the SPARK 2014 Tutorial
• More documentation can be found in the List of Resources on Ada and SPARK Ada, including
  Book John W. Mccormick: Building High Integrity Applications with Spark. Cambridge University Press September 2015. ISBN: 978-1107656840
  • Ada Core University with video tutorials about programming in Ada
  • Ada Core University Course on Spark Ada
  • Installation of SPARK Ada on your own computer
• SPARK Ada can easily be installed under Linux, Windows, and Mac OS, and probably some other operating systems, Instructions can be found here.
• Obsolete 2020/21 since why3 not used in labs
  • Advantage of Linux is that it allows to install the why3 system (which is helpful but not always necessary)
  • When we have reached verification conditions in the module, study basic usage of why3
• Main Page about SPARK Ada by Anton Setzer