SPARK Ada实现三位数减1功能及0-9范围digit类型定义问题

1. 统一Digit类型并修改参数 #

现有代码重复定义了3个范围完全一致的独立类型d1/d2/d3属于冗余设计，应该先统一定义单数字类型，再修改过程参数的类型约束：

pragma SPARK_Mode;
    
package Decrement is
    -- 统一定义0-9的数字类型，全流程复用即可
    type Digit is new Integer range 0 .. 9;
       
    -- 输入输出参数直接用Digit类型，自动限制取值范围，不需要用无约束的Integer
    procedure Dec(d1, d2, d3 : in Digit; o1, o2, o3 : out Digit);      
end Decrement;

减1逻辑核心是处理借位：从个位开始减1，遇到减完小于0的情况就置为9并向高位借1，百位如果被借位后小于0也置为9，刚好满足000输入输出999的回卷要求。

2. 封装为记录类型的实现 #

如果要把三个数位封装为独立的记录类型，可以在包内新增记录定义，调整过程的入参出参形式：

pragma SPARK_Mode;
    
package Decrement is
    type Digit is new Integer range 0 .. 9;
    -- 定义三位数字的记录类型
    type Three_Digit is record
        D1 : Digit; -- 百位
        D2 : Digit; -- 十位
        D3 : Digit; -- 个位
    end record;
       
    -- 入参出参都用记录类型，结构更清晰
    procedure Dec(Input : in Three_Digit; Output : out Three_Digit);
end Decrement;

对应的包体参考实现如下，所有操作都符合SPARK的类型安全要求：

pragma SPARK_Mode;

package body Decrement is
    procedure Dec(Input : in Three_Digit; Output : out Three_Digit) is
        Borrow : Integer := 1; -- 要减的数值为1，初始借位设为1
    begin
        -- 处理个位
        if Integer(Input.D3) - Borrow >= 0 then
            Output.D3 := Input.D3 - Digit(Borrow);
            Borrow := 0;
        else
            Output.D3 := 9;
            Borrow := 1;
        end if;
        
        -- 处理十位
        if Borrow = 1 then
            if Integer(Input.D2) - Borrow >= 0 then
                Output.D2 := Input.D2 - Digit(Borrow);
                Borrow := 0;
            else
                Output.D2 := 9;
                Borrow := 1;
            end if;
        else
            Output.D2 := Input.D2;
        end if;
        
        -- 处理百位
        if Borrow = 1 then
            if Integer(Input.D1) - Borrow >= 0 then
                Output.D1 := Input.D1 - Digit(Borrow);
            else
                Output.D1 := 9;
            end if;
        else
            Output.D1 := Input.D1;
        end if;
    end Dec;
end Decrement;

学习建议 #

• 先熟悉Ada的强类型系统设计逻辑，重点掌握自定义类型、子类型、记录类型的语法和适用场景
• 再了解SPARK中对类型约束、前置后置条件的要求，保证程序的可验证性

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