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
X-Received: by 2002:a05:6214:1cb:: with SMTP id c11mr3215476qvt.47.1630670730078;
        Fri, 03 Sep 2021 05:05:30 -0700 (PDT)
X-Received: by 2002:a5b:58e:: with SMTP id l14mr4694057ybp.143.1630670729857;
 Fri, 03 Sep 2021 05:05:29 -0700 (PDT)
Path: eternal-september.org!reader02.eternal-september.org!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 3 Sep 2021 05:05:29 -0700 (PDT)
In-Reply-To: <86r1e80zu2.fsf@stephe-leake.org>
Injection-Info: google-groups.googlegroups.com; posting-host=80.194.57.154; posting-account=xS3LTwoAAAB3aeXopC8a-M58TGE8K6go
NNTP-Posting-Host: 80.194.57.154
References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com> <86r1e80zu2.fsf@stephe-leake.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4b5164f1-71da-4581-8e02-2480e24520b9n@googlegroups.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
From: Mark Wilson <markwilson@wilsonnet.technology>
Injection-Date: Fri, 03 Sep 2021 12:05:30 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader02.eternal-september.org comp.lang.ada:62619
List-Id: <comp.lang.ada>

On Wednesday, September 1, 2021 at 10:07:41 PM UTC+1, Stephen Leake wrote:
> 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. 

No problem at all reasoning about Lengths in Spark. Here, we add the postcondition that if the result has a length of zero then the set is empty, too.

--------------------------------------------------------------------------------

   function To_Sequence
     (Set : in Character_Set)
      return Character_Sequence
     with
       Global  => null,
       Depends => (To_Sequence'Result => (Set)),
       Post    => ((if To_Sequence'Result'Length = 0 then
                      (for all k in Character'Range =>
                          Element (Set, k) = False)) and
                   (for all m in Character'Range =>
                      (if Element (Set, m) then
                         (for some n in To_Sequence'Result'Range =>
                             To_Sequence'Result(n) = m))));

--------------------------------------------------------------------------------

   function To_Sequence
     (Set : in Character_Set)
      return Character_Sequence
   is
      Result : String (1 .. Character'Pos (Character'Last) + 1)
        with Relaxed_Initialization;
      Count : Natural := 0;
   begin
      
      for Char in Set'Range loop
         
         pragma Warnings (Off);
         
         pragma Loop_Invariant
           (Count <= Character'Pos (Char));
         
         pragma Loop_Invariant
           (Result (Result'First .. Count)'Initialized);

         pragma Loop_Invariant
           (if Char > Set'First then
              (for all m in Set'First .. Character'Pred (Char) =>
                   (if Element (Set, m) then
                      (for some n in Result'First .. Count =>
                             Result(n) = m))));
         
         pragma Loop_Invariant
           (if Result'Length = 0 then
              (for all k in Set'First .. Char =>
                   Set(k) = False));
         
         pragma Warnings (On);
              
         if Set(Char) then
            Count := Count + 1;
            Result(Count) := Char;
         end if;

      end loop;
      
      return Result (1 .. Count);
      
   end To_Sequence;
   
--------------------------------------------------------------------------------