Queues, in SPARK
SPARK 2014 - Queues
This example illustrates the use of the formal container libraries in SPARK 2014. In this example the Formal_Doubly_Linked_Lists package is used to implement a container for a queue of Integers.
Authors: Claire Dross
Topics: Data Structures
Tools: SPARK 2014
References: ProofInUse joint laboratory
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
The full code is in the ZIP archive above. Here is below the specification. The proofs can be replayed using SPARK Community 2018 and invoking the test.cmd script from the archive.