Сумма квадратов в спарке

Question

Для школьного проекта я должен написать статью о языке программирования SPARK, что я и сделал, однако часть его - написать короткую программу, которая принимает целое число n и выводит сумму квадратов от 1 до n. В C++ программа будет выглядеть примерно так:

#include <iostream>
using namespace std;

int main()
{
    int n;
    cin >> n;
    if (n < 0) return 1;
    int sum = 0;
    int i = 0;
    while (i <= n) sum += i*i;
    cout << sum;
    return 0;
} 

Я совсем не знаком со SPARK, я нашел похожую программу в Ada и немного ее изменил, чтобы она работала с целыми числами, а не с двойными, и выводила бы результат (55).

with Ada.Text_IO;  use Ada.Text_IO;

procedure Test_Sum_Of_Squares is
   type Integer_Array is array (Integer range <>) of Integer;

   function Sum_Of_Squares (X : Integer_Array) return Integer is
      Sum : Integer := 0;
   begin
      for I in X'Range loop
         Sum := Sum + X (I) ** 2;
      end loop;
      return Sum;
   end Sum_Of_Squares;

begin
   Put_Line (Integer'Image (Sum_Of_Squares ((1, 2, 3, 4, 5))));
   end Test_Sum_Of_Squares;

Теперь вопрос в том, как превратить эту программу Ada в SPARK. Я попытался изменить Ada.Text_IO на Spark_IO, но IDE (GPS) дает мне "файл spark_io.ads" не найден ". Также программа должна работать с произвольным целым числом n, а не только с 5, как в примере. Любая помощь будет высоко ценится.

Answer 1

Я предполагаю, что вы используете GNAT SPARK 2014 в качестве примера программы. Ваша программа-пример уже является действующей программой SPARK.

Вы могли бы изменить Sum_Of_Squares Функция к коду ниже, чтобы вычислить сумму произвольного целого числа, которое читается на консоли. Нет необходимости использовать массив для зацикливания. Я изменил Integer в Natural, потому что я предположил, что вас интересуют только квадраты чисел, большие или равные 0.

with Ada.Text_IO;  use Ada.Text_IO;

procedure Main is
   package Nat_IO is new Integer_IO(Natural); use Nat_IO;

   function Sum_Of_Squares (X : in Natural) return Natural is
      Sum : Natural := 0;
   begin
      for I in 1 .. X loop
         Sum := Sum + I ** 2;
      end loop;
      return Sum;
   end Sum_Of_Squares;

   Input : Natural := 0;
begin
   Nat_IO.Get(Input);
   Put_Line (Positive'Image (Sum_Of_Squares (Input)));
end Main;

Тем не менее, одним из преимуществ SPARK является добавление дополнительной информации, позволяющей автоматически проверять определенные свойства вашей программы.

Надеюсь, что это помогло.