Re: Postcondition on Strings.Maps.To_Sequence

[Mark Wilson <markwilson@wilsonnet.technology>]

Good morning,

It's fairly easy to prove the positive case (level 2, latest AdaCore community edition) that if a character is in a set, it's also in a sequence

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

   function Element
     (Set   : in Character_Set;
      Value : in Character)
      return Boolean
     with
       Ghost,
       Global  => null,
       Depends => (Element'Result => (Set, Value));

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

   function Element
     (Set   : in Character_Set;
      Value : in Character)
      return Boolean
   is
     (Set (Value));

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

   function To_Sequence
     (Set : in Character_Set)
      return Character_Sequence
     with
       Global  => null,
       Depends => (To_Sequence'Result => (Set)),
       Post    => (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 Warnings (On);
              
         if Set(Char) then
            Count := Count + 1;
            Result(Count) := Char;
         end if;

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

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

The pragma Warnings (Off);  are there since the Ada compiler doesn't understand Relaxed_Initialization. We have to enclose the entire set of Loop_Invariants since Spark requires them all to be next to each other, and if we insert the pragma Warnings just around the 'Initialized invariant, we get warnings.

Of course, we turn them back on as soon as we can.

Respectively, the loop invariants prove three things, here:

(i) That count is in range
(ii) That we're initializing Result as we go along
(iii) If a character is in the Set, then it's in the sequence

This is a *partial proof*. (At least) two more things to do here:

(i) Prove that sequence is ordered - the original Ada design, whilst not specifying that the sequence is ordered, always returned it ordered, and you know - I mean you *just* know, that someone relies on that!
(ii) Prove that if a character is not in the set, then it's not in the sequence

This should get you going.

Cheers,
M