如何在SPARK Ada中无需子类型实现Integer到Digit的安全类型转换

问题1解答 #

• 可以直接通过类型内置属性引用Digit的定义范围，不需要额外定义DigitRange类型，也不需要使用IN Digit这类无效判断语句
• Digit是Integer的派生类型，其内置属性Digit'First、Digit'Last的返回值本身就是Integer类型，可直接与Integer类型的输入值比较，判断逻辑可写为：

  IF InputInteger >= Digit'First AND InputInteger <= Digit'Last THEN
      -- 范围校验通过后的后续逻辑
  END IF;
  

• 该方案的校验逻辑完全依赖Digit本身的类型定义，不需要引入额外自定义的兼容变量。

问题2解答 #

• 可以实现安全转换，只要显式给出前置的范围校验逻辑，gnatprove可以识别校验规则并消除范围检查报错，两种常用实现示例如下：

  -- 方案1：使用前置条件约束输入范围（适合调用方可控的场景）
  function Convert_To_Digit (InputInteger : Integer) return Digit with
    Pre => InputInteger >= Digit'First AND InputInteger <= Digit'Last
  is
  begin
    return Digit(InputInteger);
  end Convert_To_Digit;
  
  -- 方案2：内部做范围校验+默认值处理（适合输入不可控的场景）
  function Convert_To_Digit_Safe (InputInteger : Integer) return Digit is
  begin
    if InputInteger >= Digit'First AND InputInteger <= Digit'Last then
      return Digit(InputInteger);
    else
      -- 可根据业务需求调整默认返回值，或触发自定义错误处理逻辑
      return 0;
    end if;
  end Convert_To_Digit_Safe;
  

• 两种方案都不需要定义子类型，且gnatprove可以证明转换步骤的范围检查不会失败。

问题3解答 #

• 该方案不可行，会稳定触发range check might fail报错：
  1. SPARK的语义规则不允许产生无效值，未校验的情况下直接做类型转换，如果输入超出Digit的范围，转换步骤本身就会生成无效值，违反SPARK的数据流合法性要求，该步骤会直接被gnatprove标记风险
  2. 'Valid属性属于后置校验，gnatprove不会将后置的有效性检查回溯作为转换步骤的范围保证，无法消除转换步骤的报错。

内容的提问来源于stack exchange，提问作者Surobaki