如何在 Ada 的动态谓词中处理未初始化的数据？

Question

这是一些我没有按原样测试过的简化代码（因此它可能包含错误），展示了我遇到的问题：

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

我无法找到一种方便的方法来初始化 Nested_Space 而不会使谓词定义的断言失败。如果我尝试先设置 Inner 的成员，Outer 的成员仍然在他们默认的地方。但是，如果我尝试先将成员设置为 Outer，则 Inner 的成员仍然在他们默认的位置。即使我尝试对任一类型强制使用默认值，仍然无法选择一个肯定会在任意 Nested_Space 范围内的默认值。

甚至尝试使用类似的东西进行初始化

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

我似乎无法避免断言失败。我可以想出一些非常笨拙的想法（例如将 Initialized : Boolean 添加到 Nested_Space 专门用于检查谓词，或者设置两个不同空间的成员）但我希望可能有一个不影响的解决方案用例不需要的东西的记录结构。

如果 ARM 中没有解决方案，欢迎使用 GNAT 解决方案。

提前致谢！

Answer 1

我无法找到一种方便的方法来初始化 Nested_Space 而不会使谓词定义的断言失败。如果我尝试先设置 Inner 的成员，Outer 的成员仍然在他们默认的地方。但是，如果我尝试先将成员设置为 Outer，则 Inner 的成员仍然在它们默认的位置。

ARM 3.2.4 (35/3) 说：“Static_Predicate 与约束一样，对于子类型的所有对象始终保持 True，除非在未初始化的变量和其他无效值的情况下。另一方面，Dynamic_Predicate 会按照指定进行检查上面，但在其他时候可能会变为 False。例如，在修改子组件时不检查记录子类型的谓词。您似乎在说没有遵循这一点，并且在您分配给记录组件时会检查记录谓词。如果是这样，那么您发现了编译器错误。聚合失败似乎支持了这个想法。

但是，除非您发布一个可编译的示例来演示您的问题，否则我们无法确定这是编译器错误。