I have been generating SPARK bodies against fixed specifications and checking them with gnatprove --level=2. I have hit an obligation I cannot discharge, and I suspect I am missing a standard idiom rather than anything deep.
The spec is a cumulative product over an array, everything bounded by construction:
Max_Index : constant := 13;
Max_Value : constant := 4;
Max_Product : constant := Max_Value ** (Max_Index + 1);
subtype Index_Type is Natural range 0 .. Max_Index;
subtype Value_Type is Integer range -Max_Value .. Max_Value;
subtype Product_Type is Integer range -Max_Product .. Max_Product;
type Int_Array is array (Index_Type range <>) of Value_Type;
type Product_Array is array (Index_Type range <>) of Product_Type;
procedure Cum_Prod (A : Int_Array; Result : out Product_Array) with
Pre => Result'First = A'First and then Result'Last = A'Last
and then A'Length > 0,
Post => Result (A'First) = A (A'First)
and then (for all I in A'First + 1 .. A'Last =>
Result (I) = Result (I - 1) * A (I));
The body is the obvious one, with the prefix invariant:
Result (A'First) := A (A'First);
for I in A'First + 1 .. A'Last loop
Result (I) := Result (I - 1) * A (I);
pragma Loop_Invariant
(for all J in A'First + 1 .. I => Result (J) = Result (J - 1) * A (J));
end loop;
gnatprove says:
medium: range check might fail, cannot prove lower bound for Result (I - 1) * A (I)
Which is fair. From the subtypes alone Result (I - 1) could be Max_Product, and Max_Product * Max_Value is outside Product_Type. Nothing actually overflows — at most 14 elements each bounded by 4, so the true maximum is exactly 4**14 — but the prover has no reason to believe that.
The natural strengthening is a bound that grows with the index:
pragma Loop_Invariant
(for all J in A'First .. I => abs Result (J) <= Max_Value ** (J - A'First + 1));
That states the right thing. The preservation step is where I get stuck. Getting abs Result (I) <= Max_Value ** (I - A'First + 1) from abs Result (I - 1) <= Max_Value ** (I - A'First) needs
Max_Value ** (n + 1) = Max_Value ** n * Max_Value
and gnatprove does not appear to know that for a variable exponent. The assertion comes back as medium: assertion might fail.
Three questions.
- Is there a recognised idiom for this? My instinct is a ghost lemma procedure with the power identity as its postcondition and a null body, in the style of the manual proof sections of the User’s Guide.
- Is a bounded
Product_Typesimply the wrong modelling choice? Moving the result toBig_Integerremoves every overflow obligation and the postcondition proves cleanly, but it changes the contract from “the result fits” to “the result is correct”. Those are different promises. I am interested in which way people lean when the bound is a fact about the inputs rather than something the caller supplies. - Is there a way to give the prover the range fact without an explicit exponent — carrying a ghost variable holding the running bound, so the arithmetic stays linear?
Separately, and I may just not know where to look: is there an automated benchmark for SPARK proof work? Something a person can point a tool at and get a comparable number out of. I know of the ACATS suite for compilers and spark-by-example as a teaching corpus, but I have not found anything that plays the role a benchmark plays elsewhere. If there is nothing, I would be glad to help build one — I have a set of tasks lying around that would do for a start.
Is posting the full compilable spec and body useful for anyone?