如何执行安全类型转换检查？

Question

前言：我正在使用 GNAT 社区的最新版本（截至撰写本文时）的 SPARK Ada 进行编程。

我一直在互联网上寻找一个简单的解决方案，但所有结果似乎都指向对我不起作用的相同答案。我有一个新类型Digit定义为TYPE Digit IS new Integer range 0 .. 9. 我想安全地转换Integer为Digit. 为了进行此转换，我还创建了一个DigitRange定义为 的范围TYPE DigitRange IS range 0 .. 9。我试图通过检查是否Digit在范围 ( IF InputInteger IN DigitRange) 内来执行此转换，但这会引发不兼容的类型编译错误。

• 是否可以参考0 .. 9定义Digit类型的范围而不具体说明IF InputInteger IN Digit？因为没有子类型，IN所以不会产生有用的结果，并且 if 语句将无效。我想在代码中明确写入，我的转换不是通过检查与任意变量（例如DigitRange.
• 是否可以在不进行子类型化的情况下执行此类型转换，同时保持安全性并且不接收范围检查可能会失败错误gnatprove？
• 或者，我是否应该最初不执行检查，转换类型，然后Output'Valid作为最后的手段执行？据我了解，这仍然会给我带来范围检查，类型转换本身可能会失败。

我知道实现此目的更理想的解决方案是使用子类型，但我不允许这样做。

谢谢您的回答。

Answer 1

将 Integer'Pos 应用于 Integer 值会将其“转换”为“通用整数”，然后您可以测试它是否包含在任何整数类型的范围内：

   X : Integer;
   ...
   if Integer'Pos(X) in Digit then ...