comp.lang.ada
 help / color / mirror / Atom feed
* Postcondition on Strings.Maps.To_Sequence
@ 2021-08-29  9:38 mockturtle
  2021-09-01 21:07 ` Stephen Leake
  0 siblings, 1 reply; 6+ messages in thread
From: mockturtle @ 2021-08-29  9:38 UTC (permalink / raw)


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?

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: Postcondition on Strings.Maps.To_Sequence
  2021-08-29  9:38 Postcondition on Strings.Maps.To_Sequence mockturtle
@ 2021-09-01 21:07 ` Stephen Leake
  2021-09-02 19:17   ` mockturtle
  2021-09-03 12:05   ` Mark Wilson
  0 siblings, 2 replies; 6+ messages in thread
From: Stephen Leake @ 2021-09-01 21:07 UTC (permalink / raw)


mockturtle <framefritti@gmail.com> 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).  

<snip>

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: Postcondition on Strings.Maps.To_Sequence
  2021-09-01 21:07 ` Stephen Leake
@ 2021-09-02 19:17   ` mockturtle
  2021-09-03 11:46     ` Mark Wilson
  2021-09-03 12:05   ` Mark Wilson
  1 sibling, 1 reply; 6+ messages in thread
From: mockturtle @ 2021-09-02 19:17 UTC (permalink / raw)


On Wednesday, September 1, 2021 at 11:07:41 PM UTC+2, Stephen Leake wrote:

> 
> So just guessing; does Spark actually understand 'Length? 

I think it does, since I use it frequently in contracts (e.g. putting in some procedure the pre-condition that a string must be shorter than Positive'Last since otherwise Spark complains that I could have an overflow)

> 
> For example, can it prove "a"'Length = 1? 
> and then To_Sequence (To_Set ('a'))'Length = 1?

Good idea, I'll try this test.

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: Postcondition on Strings.Maps.To_Sequence
  2021-09-02 19:17   ` mockturtle
@ 2021-09-03 11:46     ` Mark Wilson
  2021-09-03 11:53       ` Mark Wilson
  0 siblings, 1 reply; 6+ messages in thread
From: Mark Wilson @ 2021-09-03 11:46 UTC (permalink / raw)


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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: Postcondition on Strings.Maps.To_Sequence
  2021-09-03 11:46     ` Mark Wilson
@ 2021-09-03 11:53       ` Mark Wilson
  0 siblings, 0 replies; 6+ messages in thread
From: Mark Wilson @ 2021-09-03 11:53 UTC (permalink / raw)


You'll also need to prove that each character in the sequence is unique ...

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: Postcondition on Strings.Maps.To_Sequence
  2021-09-01 21:07 ` Stephen Leake
  2021-09-02 19:17   ` mockturtle
@ 2021-09-03 12:05   ` Mark Wilson
  1 sibling, 0 replies; 6+ messages in thread
From: Mark Wilson @ 2021-09-03 12:05 UTC (permalink / raw)


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

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2021-09-03 12:05 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-08-29  9:38 Postcondition on Strings.Maps.To_Sequence mockturtle
2021-09-01 21:07 ` Stephen Leake
2021-09-02 19:17   ` mockturtle
2021-09-03 11:46     ` Mark Wilson
2021-09-03 11:53       ` Mark Wilson
2021-09-03 12:05   ` Mark Wilson

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox