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

Question

I am trying to create a decrement program in SPARK Ada. D1 to D3 are the input digits entered by the user and the program asks to decrement a 3 digit number by one and output 3 digits O1, O2, O3. I am not sure how to modify this to element of type digits. Then I will adapt it so the numbers are given as a record type consisting of 3 digits. Any help to helpful websites/explanation will be highly appreciated.

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.

This is my source code so far:

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

What behavior do you want when the value of the digit to decrement is 0? Should the result be 9? If so you want to define the digit type as a modular type

type digit is mod 10;

Your package should then be defined as:

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;

Upon looking at the package definition above you might want to consider how you really want the procedure Dec to behave. For instance, should the three in parameters actually be an array of digits? If so the output parameters can also be an array of digits. Do you want to modify the input parameters directly rather than making a decremented copy of their values? If so you should change the package definition as follows:

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;

If, on the other hand you want a decremented copy of the input values you can declare a function:

function dec(The_Digits : in digit_array) return digit_array;

If you really want the user to input a three digit number and you want to decrement each digit of the number then the package should look something like:

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

Inside the package body you will then need to isolate each digit, decrement the digit, and then return the reconstructed integer from the decremented digits.

Your description of what you need to do must be clarified so that you know what to do.

Answer 2

This is a version of a package spec that assumes that the digits we’ve dealing with represent the digits of a three-digit decimal number. If that’s not the case, then of course the code is wrong!

package Decrement with SPARK_Mode is

   type Digit is range 0 .. 9;

Now we have a convenience function to convert the digits to the corresponding Natural value. It’s marked Ghost, which means that it can only be used in SPARK-related contexts, particularly here pre- and post-conditions.

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

Now the procedure to decrement an input set of digits. I hope the parameter names are self-explanatory.

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

Now its pre- and post-conditions.

We really can’t support an input value of 0 0 0 (unless your requirements say the result should 'wrap' to 9 9 9).

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

The output needs to be 1 less than the input.

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

... and that’s that.

end Decrement;