Tokeneer Discovery: A SPARK Tutorial
Open Tokeneer With GPS
Start GPS. In the Welcome Dialog, select Open Existing Project and open
- tis_spark_tut.gpr located in the directory
tokeneer/code/core.
Check that the SPARK menu is in the menu bar. If it is not, make sure that the SPARK toolset’s bin directory is on your path, then restart GPS.
Alternately, if you did not open the project with the Welcome Dialog then select Open in the Project menu and open tis_spark_tut.gpr.
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.