Just a bit of light string manipulation today. I was surprised that there isn’t a Ada.Strings.Fixed.Index that takes a Character argument, only String or Maps.Character_Set.
I was also surprised about the missing Index function for searching a character in a string, so I briefly wrote my own
function Index (Source : String; Pattern : Character) return Natural is
begin
for I in Source'Range loop
if Source(I) = Pattern then return I; end if;
end loop;
return 0;
end Index;
In my solution I declared an array with range 'A' .. 'z' as an index. I only use 'a' .. 'z' and 'A' .. 'Z' slices of it for actual values and other elements are initialized to an default value and never change. Any ideas how to help SPARK understand it?
To be more concrete, if I comment line 49 out gnatprove complains
You need a loop invariant in the loop at line 42 that modifies Found so that GNATprove knows that Found(J) is None for the other values. Something like:
pragma Loop_Invariant
(for all J not in Rucksack_Item => Found (J) = None);