Lab Sessions Critical Systems CSCM13/High Integrity Systems CSC313
SPARK Ada can easily be installed under Linux, Windows, and Mac OS, and probably some other operating systems.
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
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