（SPARK Ada）作为 0-9 范围内数字类型的元素给出的数字？

Question

我正在尝试在 SPARK Ada 中创建一个递减程序。 D1 到 D3 是用户输入的输入数字，程序要求将一个 3 位数字减 1，输出 3 位数字 O1、O2、O3。我不确定如何将其修改为数字类型的元素。然后我将对其进行调整，以便将数字作为由 3 位数字组成的记录类型给出。对 websites/explanation 的任何帮助将不胜感激。

Eg1 of program) if d1=1 d2=2 d3=3 then output = 122. Eg2 of program) input d1=0 d2=0 d3=0 then output = 999.

这是我目前的源代码：

pragma SPARK_Mode;
    
package Decrement is
    type d1 is new Integer range 0 .. 9;
    type d2 is new Integer range 0 .. 9;
    type d3 is new Integer range 0 .. 9;
       
    procedure Dec(d1,d2,d3 : in Integer; o1,o2,o3 : out Integer);      
end Decrement;

Answer 1

当要减少的数字的值为 0 时，您想要什么行为？结果应该是9吗？如果是这样，您想将数字类型定义为模块化类型

type digit is mod 10;

您的包裹应定义为：

package Decrement is
   type digit is mod 10;
   procedure Dec (d1 : in digit; d2 : in digit; d3 : in digit;
                  o1 : out digit; o2 : out digit; o4 : out digit);
end Decrement;

查看上面的包定义后，您可能需要考虑您真正希望过程 Dec 的行为方式。例如，三个 in 参数实际上应该是一个数字数组吗？如果是这样，输出参数也可以是数字数组。您想直接修改输入参数而不是制作它们值的递减副本吗？如果是这样，您应该按如下方式更改包定义：

package Decrement is
   type digit is mod 10;
   type digit_array is array (0..2) of digit;
   procedure dec (The_Digits : in out digit_array);
end Decrement;

另一方面，如果您想要输入值的递减副本，您可以声明一个函数：

function dec(The_Digits : in digit_array) return digit_array;

如果您真的希望用户输入一个三位数，并且您希望该数字的每一位都递减，那么包应该类似于：

package Decrement is
   subtype digits_3 is Integer range 100 .. 999;
   function dec (Value : in digits_3) return digits_3;
end Decrement;

在包体中，您需要隔离每个数字，减少数字，然后 return 从减少的数字中重建整数。

必须澄清您对需要做的事情的描述，以便您知道该做什么。

Answer 2

这是一个版本的包规范，假设我们处理的数字代表三位十进制数的数字。如果不是这样，那么代码当然是错误的！

package Decrement with SPARK_Mode is

   type Digit is range 0 .. 9;

现在我们有一个方便的函数可以将数字转换为相应的 Natural 值。 It’s marked Ghost，这意味着它只能在与 SPARK 相关的上下文中使用，特别是这里的前置条件和 post 条件。

   function Val (Hundreds, Tens, Units : Digit) return Natural
   is (Natural (Hundreds) * 100 + Natural (Tens) * 10 + Natural (Units))
   with Ghost;

现在是递减一组输入数字的过程。我希望参数名称是不言自明的。

   procedure Dec (Input_Hundreds  :     Digit;
                  Input_Tens      :     Digit;
                  Input_Units     :     Digit;
                  Output_Hundreds : out Digit;
                  Output_Tens     : out Digit;
                  Output_Units    : out Digit)
   with

现在是前置条件和 post 条件。

我们真的不能支持 0 0 0 的输入值（除非你的要求说结果应该 'wrap' 到 9 9 9）。

     Pre =>
       Val (Input_Hundreds, Input_Tens, Input_Units) > 0,

输出需要比输入小1。

     Post =>
       Val (Output_Hundreds, Output_Tens, Output_Units)
       = Val (Input_Hundreds, Input_Tens, Input_Units) - 1;

...就是这样。

end Decrement;

（SPARK Ada）作为 0-9 范围内数字类型的元素给出的数字？

(SPARK Ada) Digits given as a element of type digits in range 0-9?

ada

spark-ada