SPARK Proof [title padded to meet minimum length requirement]

General
1

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.

Any insights?

2

My guess is the UR field of the CR? Try changing the CR field to integer type and adjust your “<” function and see if it proves. If it does, then that narrows it down to the UR type… If it is that, My guess is that the default discriminant might be hard for it natively since it affects the size of the record and you may need to provide a “=” function that proves in some way? I don’t do a lot of spark, so not really sure.

3

A comment on Stack Overflow led to using --level=1, which proves this.