ada - 你如何检查安全类型转换？

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定义类型的范围？因为没有子类型，不会产生有用的结果，并且 if 语句将无效。我想通过检查与任意变量（例如.DigitIF InputInteger IN DigitINDigitRange
• 是否可以在不进行子类型化的情况下执行这种类型转换，同时保持安全并且不接收范围检查可能会失败gnatprove？
• 或者，我是否应该最初不执行检查，转换类型，然后Output'Valid作为最后的手段执行？据我了解，这仍然会给我一个范围检查，类型转换本身可能会失败。

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

谢谢您的回答。

标签： ada

Answer 1

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

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