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

Posted 2023-04-12

【中文标题】如何在 Ada 的动态谓词中处理未初始化的数据？

【英文标题】：How do I handle uninitialized data in a dynamic predicate in Ada?

【发布时间】：2022-01-15 13:38:14

【问题描述】：

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

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 解决方案。

提前致谢！

【问题讨论】：

只是好奇。为什么您希望您的记录包含您标记为内部的相同值的两个实例？您的记录有一个名为内部的空间和另一个名为外部的空间，它们必须是内部的超集。创建一个函数来初始化为附加值提供 Inner 和另一个参数的记录，然后创建一个由 Inner 构造的 Outer 加上第二个参数中的附加值的记录不是更容易吗？

【参考方案1】：

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

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

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

【讨论】：

我想我在上面说错了......如果我设置空间本身，而不是它们的组件，断言会失败。但是，正如您的 ARM 摘录所暗示的那样，我似乎可以更改它们的组件。