pragma Assert (Edge.On_Input /= Null_Set);
pragma Assert (To_Sequence (Edge.On_Input)'Length > 0);
where On_Input is a Character_Set (from Ada.Strings.Maps).
SPARK accepts the first (that is, it can prove that On_Input is not
empty), but complains that cannot prove the second (that is, that the
same set converted to string can give an empty string).
My question is: is this problem due to just a "weak" contract of
To_Sequence or can actually To_Sequence return the empty string for some
non Null_Set input?
So just guessing; does Spark actually understand 'Length?
For example, can it prove "a"'Length = 1?
and then To_Sequence (To_Set ('a'))'Length = 1?
My guess is neither; Spark is simply not smart enough yet. You'll have
to add some additional intermediate assertions in the body of
To_Sequence, especially one that relates the size of On_Input to the
size of the result string.
|Location:||Huddersfield, West Yorkshire, UK|
|Nodes:||16 (2 / 14)|