SPARK formal containers -- cannot prove X < Y

General
1

Edit: Okay, this turned out to be an environmental issue. I was still running gnat 14 and gnatprove 14 and wasn’t even able to upgrade until I reset alire with “alr index –reset-community” because it was giving me an error about the index version. So, with gnat_native 15.2.1 and gnatprove 15.1.0 this works with no errors. I’ll leave the post here in case anyone else has the same problem. I also had to clear out the obj directory because it seemed to be pickup up artifacts from the older gnatprove runs.

I am revisiting a program I wrote for Advent of Code in 2022 that used a couple of the Formal containers from the SPARK library, and I am now getting a number of different errors. This is one of them:

spark-containers-parameter_checks.adb:81:10: medium: precondition might fail, cannot prove not (X < Y), in instantiation at spark-containers-functional-vectors.ads:329, in instantiation at spark-containers-formal-ordered_maps.ads:196, in instantiation at day23.adb:25
81 | Param_Eq_Transitive (X, Y, Z);

Would this have something to do with the fact that I define a “<“ function for the record I am storing? In this case it looks like:

type Coord_Type is record
X : Integer := 0;
Y : Integer := 0;
end record;

function Coord_Less (A, B : Coord_Type) return Boolean
is (A.X < B.X or else (A.X = B.X and then A.Y < B.Y));

package Coord_Set is new SPARK.Containers.Formal.Ordered_Sets (
Element_Type => Coord_Type,
“<” => Coord_Less);

package Coord_Map is new SPARK.Containers.Formal.Ordered_Maps (
Key_Type => Coord_Type, Element_Type => Natural,
“<” => Coord_Less);
2 Likes
2

For completeness shake, when GNATprove/SPARK says precondition might fail, cannot prove... that generally can also mean that it cannot find a failure but it also cannot find that it works in all cases. The way that this is usually fixed is by allowing the prover more techniques and “time”, which can easily be done by passing --level=4 as a command line argument.

Best,
Fer

2 Likes