Tokeneer Discovery: A SPARK Tutorial
Tools Installation
If you are a SPARK Pro customer, the tools can be downloaded from AdaCore’s website via GNAT Tracker. If you are a free software developer or an academic you can use the SPARK GPL toolset available on AdaCore’s Libre site. Visit the Tokeneer tools page for more information.
For GPS users, you need to also install the suitable GPS plug-in for SPARK.
- For GPS 4.4.1, Replace the file
spark.pyin the directorygnatpro/share/gps/plug-ins/with the copy in the directorytokeneer/tools/plug_ins/gps4.4.1/. - For GPS 4.3.1, Replace the file
spark.pyin the directorygnatpro/share/gps/plug-ins/with the copy in the directorytokeneer/tools/plug_ins/gps4.3.1/.
For users using versions below GPS 4.3.1, please upgrade your GPS to the latest version.
Chapters
- Introduction
- Contracts
What is Special About SPARK Contracts? - Preamble
Getting Started - Lesson 1
Dealing with Improper Initialization - Lesson 2
Identifying Ineffective Statements - Lesson 3
Validating Input - Lesson 4
SPARK Contracts - Lesson 5
Dealing with Overflow Errors - Lesson 6
Ensuring Secure Information Flow - Summary and Finding More Information
- Installing SPARK and GPS
- Starting GPS
- Running the Examiner
- Analyse Tokeneer
High-Integrity Programming 101
Download the first chapter of John Barnes’ SPARK textbook and get started on the road to safe and secure programming.