Guide to SPARK Ada Examples
An older version of these instructions can be found here
- The examples in the lecture can be found here
- The examples are the collection of the examples used in the modules
CSC313 High Integrity Systems and
CSCM13 Critical Systems.
- In the lectures the examples are flagged by writing in blue e.g. sect2c/example2c-17/
- Note that this lecture demonstrates how SPARK Ada detects mistakes.
Therefore most examples will not pass verification by SPARK Ada.
Only examples from the lecture where we demonstrated the correct code,
will pass it.
- Please check the README.txt files in the examples for additional information.
- The best thing is to download and unpack the complete
zip file of examples from the lecture
(Choose open with Ark) and then choose Action-> Extract -> Extract To and chose
a location to extract those file to.
- You can browse the files as well by going to
Collection of Examples from the Lecture There are as well zip versions of the individual examples.
- Examples in the distribution
- In the distribution there are examples of SPARK Ada programs located at
depending where it was installed initially (note you need to navigate to this
place starting from Root)
- Examples involving IO are located in
Back to main page SPARK 2014