如何处理 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;

我似乎无法阻止它断言失败。我可以想出一些相当笨重的想法（例如向 Nested_Space 添加一个 Initialized : Boolean 专门用于检查谓词，或者设置两个不同空间的成员），但我希望可能有一个不影响的解决方案用例不需要的内容的记录结构。

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

提前致谢！

Answer 1

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

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

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