Examples in Lecture

• The examples are after installation (following the instructions) are in the directory sparkAdaCodeLecture
• 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. sect3c/example3c-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.