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?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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;

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)