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?

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

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.

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

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

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