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 中找到了一个类似的程序并稍微修改了它，所以它可以使用整数而不是双精度数并输出结果（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，如示例中所示。任何帮助将不胜感激。

4

1 回答 1

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 的优点之一是添加一些额外的信息，以允许自动证明程序的已定义属性。

希望有帮助。

于 2014-05-31T18:55:06.593 回答