Advanced SPARK¶
Warning
This version of the website contains UNPUBLISHED contents.
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