Lab Sessions Critical Systems CSCM13/High Integrity Systems CSC313
Please start by following the
Instructions so that you can use SPARK Ada and why3 from the File Manager
Copy the folders
to a location where you want to work with
Reason is: Git repository updates frequently
If you work on it, updating of git repository failes due to conflict.
Should you ever get problems, move
to a new destination and set up git repository again following
Instructions for downloading Git repository with SPARK Ada code examples
Test your set up by using
Example code for testing your installation
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 Blackboard.
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
SPARK 2014 Tutorial
When we have reached verification conditions in the module, study
basic usage of why3
More documentation can be found in the
List of Resources on Ada and SPARK Ada
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.
We use Linux, because I don't know yet how to install the why3 system (which is helpful but not always necessary) under Windows.
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
Main Page about SPARK Ada by Anton Setzer