1

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

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;
4

2 回答 2

2

当要递减的数字的值为 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;

在包体内，您将需要隔离每个数字，递减该数字，然后从递减的数字中返回重构的整数。

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

于 2021-11-04T15:00:45.273 回答
1

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

package Decrement with SPARK_Mode is

   type Digit is range 0 .. 9;

现在我们有一个方便的函数将数字转换为相应的Natural值。它被标记为 Ghost，这意味着它只能在与 SPARK 相关的上下文中使用，尤其是这里的前置和后置条件。

   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

现在它的前置和后置条件。

我们真的不能支持输入值0 0 0（除非您的要求说结果应该“换行”到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;
于 2021-11-05T16:09:57.263 回答