Hi,
I found my first steps in spark endearing at first, now it’s straight up grating
procedure Count_And_Erase_Character (Buffer: in out Buffer_Type; Ch: Character; Count: out Buffer_count_type)
with Post => (for all I in Buffer'Range when Buffer'Old (I) = Ch => Buffer (I) = ' ');```
It doesn’t understand that if at each iteration, a character is blanked if previously it was equal to Ch, then obvious nothing in the string before an iteration can be Ch.
procedure Count_And_Erase_Character (Buffer: in out Buffer_Type; Ch: Character; Count: out Buffer_count_type)
with Post => (for all I in Buffer'Range => Buffer (I) /= Ch);
procedure Count_And_Erase_Character (Buffer: in out Buffer_Type; Ch: Character; Count: out Buffer_count_type) is
begin
Count := 0;
for I in Buffer'Range when Buffer (I) = Ch loop
pragma Loop_Invariant (Count < I - Buffer'First + 1 and (if I > Buffer'First then (if Buffer'Loop_Entry (I-1) = Ch then Buffer (I-1) = ' ')));
Count := @ + 1;
Buffer (I) := ' ';
end loop;
end Count_And_Erase_Character;
I tried several formulas but it doesn’t work. At least this last one, in the body, succeeded at proving the loop_invariant, but even though I copied equation (with 'Old instead of 'Loop_entry) it doesn’t check out.
also, i’m certain there are simpler ways to write down these assertions. I’m all ears, this is new to me.
The type defines as such:
Maximum_Buffer_Size : constant := 1024;
subtype Buffer_Count_Type is Natural range 0 .. Maximum_Buffer_Size;
subtype Buffer_Index_Type is Positive range 1 .. Maximum_Buffer_Size;
type Buffer_Type is array (Buffer_Index_Type) of Character;
When your postcondition quantifies over an array, usually the loop invariant has to as well. Right now, your loop invariant only speaks about the current iteration, but you need to summarize what has happened until then in the loop to the entire array. Something like that:
pragma Loop_Invariant (Count <= I - Buffer'First and (for all K in Buffer'First .. I - 1 => (if Buffer'Loop_Entry (K) = Ch then Buffer (K) = ' ')));
Oh, thank you for the tips.
Hey, considering the definition
subtype Buffer_Count_Type is Natural;
subtype Buffer_Index_Type is Buffer_Count_Type range 1..Buffer_Count_Type'Last;
type Buffer_Type is array (Buffer_Index_Type range <>) of Character;
procedure Copy_Into (Buffer : out Buffer_Type;
Source : in String) is
Characters_To_Copy : Buffer_Count_Type;
begin
pragma Assert (Buffer'Last in Buffer_index_type);
Characters_To_Copy := Buffer'Last;
Buffer := (others => ' '); -- initialize to all blanks
if Source'Length < Characters_To_Copy then
Characters_To_Copy := Source'Length;
end if;
for Index in Buffer'First .. Characters_To_Copy loop
pragma Loop_Invariant (Index <= Source'Length
and Characters_To_Copy = Characters_To_Copy'Loop_Entry);
Buffer (Index) := Source (Source'First + (Index - 1));
end loop;
end Copy_Into;
Does the complaint buffers.adb:30:22: medium: assertion might fail, cannot prove lower bound for Buffer'Last in Buffer_index_type makes any sense ? It can’t prove that an array’s bound fits into its OWN index subtype ?
It has to support empty arrays for the type as well. Consider the following:
with Ada.Text_IO; use Ada.Text_IO;
procedure jdoodle is
subtype Buffer_Count_Type is Natural;
subtype Buffer_Index_Type is Buffer_Count_Type range 1..Buffer_Count_Type'Last;
type Buffer_Type is array (Buffer_Index_Type range <>) of Character;
v : Buffer_Type(1..0); -- Empty array with no elements
begin
Put_Line("Last =" & v'Last'Image);
end jdoodle;
It makes sense, but then what type is 'Last in that case ? Your exemple throws no exception, yet the rm says:
A’Last For a prefix A that is of an array type (after any implicit dereference), or denotes a constrained array subtype: A’Last denotes the upper bound of the first index range; its type is the corresponding index type.
Not a base type, not a universal numeric type, but the index type.
It may have something to do with section 14 of 3.6:
I’m not a language lawyer by any means but there is also verbiage talking about resolving the type of the index to root integer, and the RM specifically calls the index part a “subtype” so it may be that the language is allowed to further go down the type liniage to handle out of bounds indexes. That’s speculation on my part though, I don’ t know.
Please do not confuse a type and its first subtype. Types are anonymous in Ada, what you declare in a type declaration is the first subtype. So the index type is the type of the first subtype Buffer_Index_Type.
The type of, e.g., Integer is the full range of mathematical integers. Static expressions make use of this: Static: constant := Integer'Last + Integer'Last;
“+” is the operator of Integer (not universal_integer). Static: constant := Integer'Last + Long_Integer'Last;
This is illegal, there is no such operator.
Ok, so we’re dealing with an unconstrained array, right?
There’s a concept in Ada called the null array, that is an array of length zero, and it is denoted with any array which has 'First strictly greater-than 'Last.
This is a little bit of a rough-spot in Ada, insofar as compiler creators are concerned, because you are required to preserve the bounds —this means that you can pass information in a null array, such as P: Example_Array:= (-12..-32 => <>), and P'First must equal -12 and P'Last must equal -32— now, obviously this is a Bad Idea™, but is technically doable.
The reason that this is such a pain is because, (a) say given Type Example_Array is (Unsigned_8 range <>) of Character;, this means that the number of ways to represent the null array are the combinatorial explosion of 1*2*3*…*254 rather than just a single conceptual null array, and (b) the leaking of information [preservation of values] illustrated above means that some care must be made WRT optimization.
But, as to why Val : Array(Positive range <>) of Positive:= (1..0 => 1); doesn’t throw an exception is because of the practical reason of recursion: you don’t want to raise an exception when your conceptual “grab half the array and process X, recursively” bottoms out on an array of length-0 (the other base-case typically being length-1). — The language-lawyer reason is because the subtype (here Positive) is an subset of Integer the array type being a conceptual Universal_Array_of_Positive_Indexed_by_Integer with the first subtype being Universal_Array_of_Positive_Indexed_by_Integer with Index in Positive'Range: thus Val is specified as Universal_Array_of_Positive_Indexed_by_Integer, but having a length-0, there is no Index which violates the constraint and thus the object is valid. (IIUC)
pragma Overflow_Mode (minimized);
pragma Ada_2022;
with Ada.Text_IO; use Ada.Text_IO;
procedure main with Spark_Mode is
Maximum_Buffer_Size : constant := 1024;
subtype Buffer_Count_Type is Natural range 0 .. Maximum_Buffer_Size;
subtype Buffer_Index_Type is Positive range 1 .. Maximum_Buffer_Size;
type Buffer_Type is array (Buffer_Index_Type) of Character;
procedure Copy_From (Buffer : in Buffer_Type;
Destination : out String;
Point : in Buffer_Index_Type;
Length : in Buffer_Count_Type)
with Depends => (Destination =>+ (Buffer, Point, Length)),
Post => (if Point not in Buffer'Range or Point + Length - 1 > Buffer'Last then (for all A of Destination => A = ' ')
else Destination (Destination'First .. Destination'First + Positive'Min (Length, Destination'Length) - 1) = String (Buffer (Point .. Point - 1 + Positive'Min (Length, Destination'Length))));
procedure Copy_From (Buffer : in Buffer_Type;
Destination : out String;
Point : in Buffer_Index_Type;
Length : in Buffer_Count_Type) is
begin
Destination := (others=> ' ');
if Point not in Buffer'Range or Point + Length - 1 > Buffer'Last then
return;
else
Destination (Destination'First .. Destination'First + Positive'Min (Length, Destination'Length) - 1) := String (Buffer (Point .. Point - 1 + Positive'Min (Length, Destination'Length)));
end if;
end Copy_From;
begin
null;
end main;
The expression in the postcondition and body are nearly identical. I would have used an expression function but there’s no way to easily “insert” an array in another with an expression. Eitherway, this should work, since it doesn’t complain about the body.
Ok, can you see what’s wrong here ?
It can not prove the postcondition, but does not complain about the loop invariant, despite it saying exactly the same thing (I copied and pasted it !!).
And here i can’t prove that the loop that erases a certain character, does remove that character:
both the invariant and postcondition (Post => (for all A of Buffer => A /= Erase_Character)) that says the same thing, fails to prove. That said, I am yet to read the guide in details. I will.
pragma Overflow_Mode (minimized);
pragma Ada_2022;
procedure main with Spark_Mode is
subtype Buffer_Count_Type is Natural;
subtype Buffer_Index_Type is Buffer_Count_Type range 1..Buffer_Count_Type'Last;
type Buffer_Type is array (Buffer_Index_Type range <>) of Character;
function Search (Haystack: Buffer_Type; Needle: String) return Buffer_Count_Type
with Post =>
((if Search'result = 0 then Needle'Length not in 1..Haystack'Length or
(for all I in Haystack'First..HayStack'Last - Needle'Length + 1 => Haystack (I..I+Needle'Length-1) /= Buffer_type(Needle))
else Haystack(Search'Result..Search'Result+Needle'Length-1) = Buffer_type(Needle)
and (for all I in Haystack'First..Search'Result-1 => Haystack(I..I+Needle'Length-1) /= Buffer_type(Needle))));
function Search (Haystack: Buffer_Type; Needle: String) return buffer_count_type is
begin
if Needle'Length not in 1..Haystack'Length then return 0; end if;
for I in Haystack'First..HayStack'Last - Needle'Length + 1
when String (haystack (I..I+Needle'Length-1)) = Needle loop
pragma Loop_invariant ((if I > Haystack'First then (for all J in Haystack'First .. I - 1 => String (Haystack(J..J+Needle'Length-1)) /= Needle)));
return I;
end loop;
return 0;
end Search;
begin
null;
end main;
procedure Compact (Buffer: in out Buffer_type; Erase_Character, Fill_Character: Character; Valid: out Buffer_Count_Type) is
Index: Buffer_Count_type := 0;
begin
Valid := Buffer'Length;
if Valid = 0 then return;
else
while Index < Buffer'Length loop
pragma Loop_Invariant (Index in 0..Buffer'Length-1 and Valid in 1..Buffer'Length);
pragma Loop_Invariant ((for all I in Buffer'First..Buffer'First+Index-1 => Buffer(I) /= Erase_character));
if Buffer (Buffer'First + Index) = Erase_Character then
Buffer (Buffer'First + Index .. Buffer'Last - 1 - Buffer'Length + Valid) := Buffer (Buffer'First + Index+1..Buffer'Last- Buffer'Length + Valid);
Valid := @ - 1;
else
Index := @ + 1;
end if;
exit when Valid = 0;
end loop;
if Valid < Buffer'Length then
pragma Assert (Valid in 0.. Buffer'Length);
Buffer (Buffer'First + Valid .. Buffer'Last) := [others => Fill_Character];
end if;
end if;
end Compact;
