0

学校のプロジェクトでは、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 で同様のプログラムを見つけて少し修正したので、double ではなく整数で動作し、結果 (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) で「file spark_io.ads」が見つかりませんでした。また、プログラムは、例のように 5 だけでなく、任意の整数 n でも動作するはずです。よろしくお願いします。

4

1 に答える 1

1

サンプル プログラムに GNAT SPARK 2014 を使用していると仮定します。サンプル プログラムは、すでに有効な SPARK プログラムです。

関数を以下のコードに変更Sum_Of_Squaresして、コンソールに読み込まれた任意の整数の合計を計算できます。ループオーバーするために配列を使用する必要はありません。を に変更しました。これは、0 以上の数の 2 乗だけに関心があると想定したためですInteger。Natural

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 の利点の 1 つは、追加情報を追加して、プログラムの定義済みプロパティを自動的に証明できるようにすることです。

それが役に立ったことを願っています。

于 2014-05-31T18:55:06.593 に答える