I’m learning SPARK by verifying a ring buffer implementation, and am having some trouble expressing the Pop function, which removes the last element.
Without any consideration for SPARK, it would look like this, raising an exception if the buffer is empty:
function Pop (B : in out Buffer) return Element;
To make this compatible, I’ve decided to return a variant record expressing an optional element, rather than raising an exception.
type Optional_Element (Init : Boolean) is record
case Init is
when True =>
V : Element;
when False =>
null;
end case;
end record;
function Pop (B : in out Buffer) return Optional_Element;
Then, since SPARK functions cannot have side effects, I tried to turn this into a procedure with an out parameter, but ran into a failed discriminant check since the Optional_Element object exists prior to the function call thus its discriminant cannot be mutated, and it seems I can’t reassign the object (see this post).
-- Incorrect, V's discriminant is fixed and cannot be reassigned during the call.
procedure Pop (B : in out Buffer; V : out Optional_Element);
I believe your Init : Boolean discriminant needs := False/True as a default to make it always exist by default and be mutatable within it’s occupied space.
For Spark personally I would tie the buffer size and Index together with a type. This way Spark knows the index will always be within the buffer size.
type Optional_Element (Init : Boolean := True) is record
case Init is
when True =>
V : Element;
when False =>
null;
end case;
end record;
Thank you, I didn’t know you could make the discriminant mutable! This works in practice, however gnatprove still seems unconvinced.
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
ring_buffer_core.adb:93:12: medium: discriminant check might fail, in instantiation at tempo_tapper.ads:27
93 | V := (Init => False);
| ~~^~~~~~~~~~~~~
ring_buffer_core.adb:97:09: medium: discriminant check might fail, in instantiation at tempo_tapper.ads:27
97 | V := (Init => True, V => Value);
| ~~^~~~~~~~~~~~~~~~~~~~~~~~
I consulted this table of messages reported by SPARK, which says this for discriminant checks:
Check that the discriminant of the given discriminated record has the expected value. For variant records, this can happen for a simple access to a record field. But there are other cases where a fixed value of the discriminant is required.
However, Pop isn’t checking individual fields, at least explicitly, it’s fully setting the value: V := .... I’m not sure what else SPARK is seeing here?
For context, my actual function looks like this. I’m not sure the details here are too important.
-- Specification
procedure Pop (B : in out Buffer; V : out Optional_Element);
function Is_Empty (B : Buffer) return Boolean;
procedure Pop_Unchecked (B : in out Buffer; V : out Element)
with Pre => not Is_Empty (B);
-- Body
procedure Pop (B : in out Buffer; V : out Optional_Element) is
Value : Element;
begin
if Is_Empty (B) then
V := (Init => False);
return;
end if;
Pop_Unchecked (B, Value);
V := (Init => True, V => Value);
end Pop;
Result : Optional_Element (Init => True);
...
Pop (B => Buffer, V => Result);
When the variable is declared with an explicit discriminant, the variable is constrained and the discriminant cannot be changed. Thus the out parameter of an unconstrained record type cannot be used in SPARK. You could use two out parameters, or a record with two normal fields, but those have other problems.
Really, the SPARK way is for Pop to be what you’ve called Pop_Unchecked, with the precondition that the Buffer is not empty. Then it’s up to the caller to ensure that Pop isn’t called with an empty Buffer, and SPARK can prove things about it.
Parameter names should be chosen so that they read well when used with named notation. I would probably have chosen
procedure Pop (From : in out Buffer; Item : out Element);
It’s probably a bit of a pain, but you could also try to wrap your optional type with a record:
type Optional_Element (Init : Boolean := True) is record
case Init is
when True => V : Element;
when False => null;
end case;
end record;
type Result is record -- Name it something better. Just quick and dirty example
Value : Optional_Element;
end record;
procedure Pop (B : in out Buffer; V : out Result);
I don’t have spark to test with here, but it might get you past the situation where someone could specify a discriminant for the value passed in.
Thanks all for the tips! I think I’ll take the route of adding preconditions.
Is there a way to mark this question as answered?
@JC001 If I understand correctly, then this should fail? It certainly fails without the default discriminant value, but with it (in the code below), the discriminant seems to be mutable even when explicitly initialized.
procedure Main is
subtype Element is Integer;
type Optional_Element (Init : Boolean := False) is record
case Init is
when True => Item : Element;
when False => null;
end case;
end record;
procedure Set_Value (Option : out Optional_Element; Value : Element) is
begin
Option := (Init => True, Item => Value);
end;
procedure Clear_Value (Option : out Optional_Element) is
begin
Option := (Init => False);
end;
O : Optional_Element := (Init => False);
begin
Set_Value (O, 23);
Clear_Value (O);
end;
Why do so many people do this?
If you have a non-discriminated type, why aren’t you using an unconstrained array?
-- We need a singular-value index, with room for a null-range.
Subtype Optional_Index is Boolean range True..True;
-- Optional is an unconstrained array with one or zero elements.
Type Optional is Array (Optional_Index range <>) of WHATEVER;
Function Has_Element( Object : Optional ) return Boolean is
( Object'Length in Positive );
Now, what you do is you put your process in a for-loop:
-- Because Optional is an unconstrained array with one or zero elements, this is safe.
For X of Optional_Value loop
Whatever_Operation( X );
End loop;
There you are.
A simple optional type, that is usable w/o much pain in SPARK.
The use of the unconstrained variant record should fail SPARK proof.
Note the difference between
Result : Optional_Element (Init => True);
and
O : Optional_Element := (Init => False);
In the former, Result has constrained subtype Optional_Element (Init => True), while the latter has unconstrained subtype Optional_Element which is then initialized with the aggregate. So your example has an unconstrained object and the discriminant can be changed. If I change the declaration of O in your example, then I get
They do it because it is clear. Clarity is the second-most important attribute of good software, after correctness. The reader understands immediately what the writer was trying to do.
The unconstrained array approach is a trick, and like most tricks, is less clear. The typical reader will wonder why an array is being used, and have to expend extra effort to understand it.
Also, an unconstrained array will not work for this purpose as an out parameter.
You wouldn’t, you’d use a discriminated record for that.
I’ll have to think on this a bit, but I don’t see it as a trick: you’re saying that you’re going to be getting a list of 0 or 1 values: the array.
OTOH, very often the whole “optional type” thing is [IIUC] from functional programming, though typically through a curly-brace language’s adoption, and deals with… a state of zero or one values.