Advanced SPARK
Warning
This version of the website contains UNPUBLISHED contents. Please do not share it externally!
This course will teach you advanced topics of SPARK.
Note
The code examples in this course use an 80-column limit, which is a typical limit for Ada code. Note that, on devices with a small screen size, some code examples might be difficult to read.
Contents:
- Subprogram Contracts
- Subprogram Contracts in Ada 2012 and SPARK 2014
- Dynamic Execution of Subprogram Contracts
- Dynamic Behavior when Subprogram Contracts Fail
- Precondition
- Postcondition
- Contract Cases
- Attribute
'Old - Implication and Equivalence
- Reasoning by Cases
- Universal and Existential Quantification
- Expression Functions
- Code Examples / Pitfalls
- Type Contracts
- Systems Programming
- Type Contracts in Ada 2012 and SPARK 2014
- Systems Programming – What is it?
- Systems Programming – How can SPARK help?
- Systems Programming – A trivial example
- Volatile Variables and Volatile Types
- Flavors of Volatile Variables
- Constraints on Volatile Variables
- Constraints on Volatile Functions
- State Abstraction on Volatile Variables
- Constraints on Address Attribute
- Can something be known of volatile variables?
- Other Concerns in Systems Programming
- Code Examples / Pitfalls
- Concurrency
- Concurrency ≠ Parallelism
- Concurrent Program Structure in Ada
- The problems with concurrency
- Ravenscar – the Ada solution to concurrency problems
- Concurrent Program Structure in Ravenscar
- Ravenscar – the SPARK solution to concurrency problems
- Concurrency – A trivial example
- Setup for using concurrency in SPARK
- Tasks in Ravenscar
- Communication Between Tasks in Ravenscar
- Protected Objects in Ravenscar
- Protected Communication with Procedures & Functions
- Blocking Communication with Entries
- Relaxed Constraints on Entries with Extended Ravenscar
- Interrupt Handlers in Ravenscar
- Other Communications Between Tasks in SPARK
- Data and Flow Dependencies of Tasks
- State Abstraction over Synchronized Variables
- Synchronized Abstract State in the Standard Library
- Code Examples / Pitfalls
- Object-oriented Programming
- Ghost code
- What is ghost code?
- Ghost code – A trivial example
- Ghost variables – aka auxiliary variables
- Ghost variables – non-interference rules
- Ghost statements
- Ghost procedures
- Ghost functions
- Imported ghost functions
- Ghost packages and ghost abstract state
- Executing ghost code
- Examples of use
- Extreme proving with ghost code – red black trees in SPARK
- Positioning ghost code in proof techniques
- Code Examples / Pitfalls
- Test and Proof