Introduction To SPARK

This tutorial is an interactive introduction to the SPARK programming language and its formal verification tools. You will learn the difference between Ada and SPARK and how to use the various analysis tools that come with SPARK.

This document was prepared by Claire Dross and Yannick Moy.

Download PDF Download EPUB

Contents:

• Overview
  • What is it?
  • What do the tools do?
  • Key Tools
  • A trivial example
  • The Programming Language
  • Limitations
    • No side-effects in expressions
    • No aliasing of names
  • Designating SPARK Code
  • Code Examples / Pitfalls
    • Example #1
    • Example #2
    • Example #3
    • Example #4
    • Example #5
    • Example #6
    • Example #7
    • Example #8
    • Example #9
    • Example #10
• Flow Analysis
  • What does flow analysis do?
  • Errors Detected
    • Uninitialized Variables
    • Ineffective Statements
    • Incorrect Parameter Mode
  • Additional Verifications
    • Global Contracts
    • Depends Contracts
  • Shortcomings
    • Modularity
    • Composite Types
    • Value Dependency
    • Contract Computation
  • Code Examples / Pitfalls
    • Example #1
    • Example #2
    • Example #3
    • Example #4
    • Example #5
    • Example #6
    • Example #7
    • Example #8
    • Example #9
    • Example #10
• Proof of Program Integrity
  • Runtime Errors
  • Modularity
    • Exceptions
  • Contracts
    • Executable Semantics
    • Additional Assertions and Contracts
  • Debugging Failed Proof Attempts
    • Debugging Errors in Code or Specification
    • Debugging Cases where more Information is Required
    • Debugging Prover Limitations
  • Code Examples / Pitfalls
    • Example #1
    • Example #2
    • Example #3
    • Example #4
    • Example #5
    • Example #6
    • Example #7
    • Example #8
    • Example #9
    • Example #10
• State Abstraction
  • What's an Abstraction?
  • Why is Abstraction Useful?
  • Abstraction of a Package's State
  • Declaring a State Abstraction
  • Refining an Abstract State
  • Representing Private Variables
  • Additional State
    • Nested Packages
    • Constants that Depend on Variables
  • Subprogram Contracts
    • Global and Depends
    • Preconditions and Postconditions
  • Initialization of Local Variables
  • Code Examples / Pitfalls
    • Example #1
    • Example #2
    • Example #3
    • Example #4
    • Example #5
    • Example #6
    • Example #7
    • Example #8
    • Example #9
    • Example #10
• Proof of Functional Correctness
  • Beyond Program Integrity
  • Advanced Contracts
    • Ghost Code
    • Ghost Functions
    • Global Ghost Variables
  • Guide Proof
    • Local Ghost Variables
    • Ghost Procedures
    • Handling of Loops
    • Loop Invariants
  • Code Examples / Pitfalls
    • Example #1
    • Example #2
    • Example #3
    • Example #4
    • Example #5
    • Example #6
    • Example #7
    • Example #8
    • Example #9
    • Example #10