Abstract models and refinement in SPARK: allocators example
This program demonstrates how the specification of a SPARK program can be formalized using an abstract model and how the refinement relation between the model an its implementation can be verified using GNATprove. It is described in the article Abstract Software Specifications and Automatic Proof of Refinement” published at RSSRail 2016 conference.
The example contains three versions of an allocator package. They are specified in terms of mathematical structures (sequences and sets). The refinement relation between the mathematical model and the implementation is expressed as a ghost function Is_Valid and enforced through contracts. It can be verified automatically using GNATprove.
Simple_Allocator features a naive implementation of the allocator, storing the status (available or allocated) of each resource in a big array. It is specified using a ghost function Model which always returns a valid refinement of the allocator’s data. The refinement relation is verified only once, as a postcondition of the Model function. List_Allocator introduces a free list to access more efficiently the first available resource. Here not every possible state of the allocator data can be refined into a valid model. To work around this problem, the model is stored in a global ghost variable which is updated along with the allocator’s data and the refinement relation is expressed as an invariant that must be verified as a postcondition of each modifying procedure. The functional contracts on modifying procedures are straightforward but the refinement relation is now more complicated, as it needs to account for the implementation of the free list. List_Mod_Allocator features the same implementation and contracts as List_Allocator, but its model is returned by a ghost function like in Simple_Allocator instead of being stored in a global ghost variable. As not every possible state of the allocator can be refined into a valid model, the refinement relation is not expressed as a postcondition of Model, but as an invariant, as in List_Allocator and must be verified as a postcondition of each modifying procedure. The functional contracts and the refinement relation resemble those of List_Allocator. However, as we don’t construct explicitly the new model after each modification, the proof of the allocator’s functional contracts requires induction, which is beyond the reach of automatic solvers. The induction scheme is given here manually in an auto-active style through calls to ghost procedures.
Authors: Claire Dross
Topics: Ghost code
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 are below the specifications of the simple allocator, the others may be found in the archive. The proofs can be replayed using SPARK Community 2018 and invoking the test.cmd script from the archive.