Re: Postcondition on Strings.Maps.To_Sequence

[Stephen Leake <stephen_leake@stephe-leake.org>]

mockturtle <framefritti@gmail.com> writes:

>    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).  

<snip>

I have used Spark some, but am not an expert.

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 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?

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.

-- 
-- Stephe