Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.ada > #49381

Re: Postcondition on Strings.Maps.To_Sequence

Show all headers | View raw

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

Back to comp.lang.ada | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Postcondition on Strings.Maps.To_Sequence mockturtle <framefritti@gmail.com> - 2021-08-29 02:38 -0700
  Re: Postcondition on Strings.Maps.To_Sequence Stephen Leake <stephen_leake@stephe-leake.org> - 2021-09-01 14:07 -0700
    Re: Postcondition on Strings.Maps.To_Sequence mockturtle <framefritti@gmail.com> - 2021-09-02 12:17 -0700
      Re: Postcondition on Strings.Maps.To_Sequence Mark Wilson <markwilson@wilsonnet.technology> - 2021-09-03 04:46 -0700
        Re: Postcondition on Strings.Maps.To_Sequence Mark Wilson <markwilson@wilsonnet.technology> - 2021-09-03 04:53 -0700
    Re: Postcondition on Strings.Maps.To_Sequence Mark Wilson <markwilson@wilsonnet.technology> - 2021-09-03 05:05 -0700

csiph-web