From: mockturtle <framefritti@gmail.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
Date: Thu, 2 Sep 2021 12:17:26 -0700 (PDT) [thread overview]
Message-ID: <4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com> (raw)
In-Reply-To: <86r1e80zu2.fsf@stephe-leake.org>
On Wednesday, September 1, 2021 at 11:07:41 PM UTC+2, Stephen Leake wrote:
>
> So just guessing; does Spark actually understand 'Length?
I think it does, since I use it frequently in contracts (e.g. putting in some procedure the pre-condition that a string must be shorter than Positive'Last since otherwise Spark complains that I could have an overflow)
>
> For example, can it prove "a"'Length = 1?
> and then To_Sequence (To_Set ('a'))'Length = 1?
Good idea, I'll try this test.
next prev parent reply other threads:[~2021-09-02 19:17 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-08-29 9:38 Postcondition on Strings.Maps.To_Sequence mockturtle
2021-09-01 21:07 ` Stephen Leake
2021-09-02 19:17 ` mockturtle [this message]
2021-09-03 11:46 ` Mark Wilson
2021-09-03 11:53 ` Mark Wilson
2021-09-03 12:05 ` Mark Wilson
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox