In SparkRC I created some higher-level data structures on top of the
Ada.Containers.Formal_* components, mainly to try to improve my understanding of how to get SPARK to prove things. Pkg spec prove.ads contains instantiations of these for various kinds of types to allow proofs. All of them prove completely, but as noted, the current predicates do not include proof of functional correctness. This is because proof of even very simple and obvious functional-correctness predicates fail for at least some of the types in prove.ads.
Consider, for example, the bounded-queue component. The Get operation is supposed to remove the head of the queue and put it in the Item parameter. This implies that the length of the queue will decrease and Item will contain the old head. Currently only the first part of that is being proved. Since the Peek function returns the head of a queue, I would like to add
Item = Peek (From)'Old
to the postcondition. In fact, doing so works with the instantiations for Integer and CA, but fails for CR. SPARK is unable to prove that part of the postcondition in that case. I am unable to see why or how to phrase this so that it can prove it.
3 posts - 2 participants