Re: Postcondition on Strings.Maps.To_Sequence

[Mark Wilson <markwilson@wilsonnet.technology>]

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;
   
--------------------------------------------------------------------------------