Search code examples
adapredicategnat

How do I handle uninitialized data in a dynamic predicate in Ada?


This is some simplified code I haven't tested as is (so it may contain errors) that demonstrates the problem I'm experiencing:

type Space is private;

--Depending on members of Space, determines whether Outer fully contains Inner
function Contains(Outer : Space; Inner : Space);

--Outer should fully contain Inner
type Nested_Space is
record
    Inner : Space;
    Outer : Space;
end record
with Dynamic_Predicate => Contains(Outer, Inner);

I haven't been able to find a convenient way to initialize a Nested_Space without failing the assert defined by the predicate. If I try to set the members of Inner first, the members of Outer are still wherever they defaulted. But if I try to set the members out Outer first, the members of Inner are still wherever they defaulted. Even if I tried forcing a default on either type, there's still no way to pick a default that will certainly be within the bounds of any arbitrary Nested_Space.

Even trying to initialize with something like

declare
    My_Inner : Space := (...);
    My_Outer : Space := (...);
    My_NS : Nested_Space := (Inner => My_Inner, Outer => My_Outer);
begin
    ....
end;

I can't seem to keep it from failing the assert. I can come up with some pretty clunky ideas (such as adding an Initialized : Boolean to Nested_Space specifically to check in the predicate, or alternatively setting members of the two different Spaces) but I was hoping there might be a solution that doesn't affect the structure of the record for something not required for the use case.

GNAT solutions are welcome if there's no solution in the ARM.

Thanks in advance!


Solution

  • I haven't been able to find a convenient way to initialize a Nested_Space without failing the assert defined by the predicate. If I try to set the members of Inner first, the members of Outer are still wherever they defaulted. But if I try to set the members out Outer first, the members of Inner are still wherever they defaulted.

    ARM 3.2.4 (35/3) says, "A Static_Predicate, like a constraint, always remains True for all objects of the subtype, except in the case of uninitialized variables and other invalid values. A Dynamic_Predicate, on the other hand, is checked as specified above, but can become False at other times. For example, the predicate of a record subtype is not checked when a subcomponent is modified." You seem to be saying that this is not followed, and the record predicate is checked when you assign to a record component. If so, then you have found a compiler error. That it fails for an aggregate seems to support this idea.

    However, unless you post a compilable example that demonstrates your problem, we cannot be sure that this is a compiler error.