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=0.8 required=3.0 tests=BAYES_50,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.6
X-Received: by 2002:a05:6214:922:: with SMTP id dk2mr18213866qvb.36.1630229928064;
        Sun, 29 Aug 2021 02:38:48 -0700 (PDT)
X-Received: by 2002:a25:bc10:: with SMTP id i16mr16229962ybh.73.1630229927833;
 Sun, 29 Aug 2021 02:38:47 -0700 (PDT)
Path: eternal-september.org!reader02.eternal-september.org!weretis.net!feeder8.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sun, 29 Aug 2021 02:38:47 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=217.56.127.6; posting-account=9fwclgkAAAD6oQ5usUYhee1l39geVY99
NNTP-Posting-Host: 217.56.127.6
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com>
Subject: Postcondition on Strings.Maps.To_Sequence
From: mockturtle <framefritti@gmail.com>
Injection-Date: Sun, 29 Aug 2021 09:38:48 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader02.eternal-september.org comp.lang.ada:62570
List-Id: <comp.lang.ada>

Dear.all,
in a code that I am trying to prove with SPARK I have the following two consecutive lines  [I am a beginner with SPARK and I am trying to learn... it is quite fun, if you have masochistic tendencies... ;-)] 

   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).  Actually, the contract of To_Sequence looks like 

function To_Sequence (Set : Character_Set) return Character_Sequence with
     Post =>
       (if Set = Null_Set then To_Sequence'Result'Length = 0)
          and then
       (for all Char in Character =>
          (if Is_In (Char, Set)
           then (for some X of To_Sequence'Result => Char = X)))
          and then
       (for all Char of To_Sequence'Result => Is_In (Char, Set))
          and then
       (for all J in To_Sequence'Result'Range =>
          (for all K in To_Sequence'Result'Range =>
             (if J /= K
              then To_Sequence'Result (J) /= To_Sequence'Result (K))));

and it shows clearly that if the input is Null_Set, then the output is the empty string, but does no explicit claim about the opposite case (if the input is not empty, then the output is not empty as well).

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?