From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on ip-172-31-74-118.ec2.internal X-Spam-Level: X-Spam-Status: No, score=-1.9 required=3.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.6 Path: eternal-september.org!reader02.eternal-september.org!aioe.org!9CzwYWWlKVx8RMZd/VcwFg.user.46.165.242.75.POSTED!not-for-mail From: Stephen Leake Newsgroups: comp.lang.ada Subject: Re: Postcondition on Strings.Maps.To_Sequence Date: Wed, 01 Sep 2021 14:07:33 -0700 Organization: Aioe.org NNTP Server Message-ID: <86r1e80zu2.fsf@stephe-leake.org> References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: gioia.aioe.org; logging-data="29840"; posting-host="9CzwYWWlKVx8RMZd/VcwFg.user.gioia.aioe.org"; mail-complaints-to="abuse@aioe.org"; User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (windows-nt) Cancel-Lock: sha1:1gqdGx8cEVXbVT3RtQQCBBYYlvI= X-Notice: Filtered by postfilter v. 0.9.2 Xref: reader02.eternal-september.org comp.lang.ada:62600 List-Id: mockturtle 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). 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