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
Basic Usage Instructions for SPARK Ada
The lab sheet and the coursework can be found under Blackboard.
It is recommended to first download 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
Once you have verified programs involving verification conditions study
basic usage of why3
More documentation can be found
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
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