Independent SPARK Support

There are two tutorials - they are both currently up-to-date with the GPL 2010 version of SPARK :

  • for the proof of absence of run-time error (using the optional proof annotations);
    comprising twelve sections with worked examples and exercises    :
    1. Introduction
    2. Using the Tools
    3. What VCs are Generated
    4. VCs for Multiple Paths
    5. Preconditions and Postconditions
    6. check and assert Annotations
    7. Loops
    8. Loop Assertions
    9. Loops, Arrays and Quantification
    10. Real RTC Analysis
    11. User Rules
    12. Proof Functions and Abstract Proof
  • for the SPADE Proof Checker; this has eight sections with worked examples and exercises:
    1. Using the Checker and the Infer Command
    2. The Replace Command
    3. Prolog Variables and the where Clause
    4. Standardisation
    5. Proof Management
    6. Proof Methods and Proof Frames
    7. Quantified Formulae
    8. Miscellaneous Topics: Subgoaling and Proof of User Rules

Both tutorials are available from the Download page.