Wiki Agenda Contact Version française

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.