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