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

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