Sum of Squares in SPARK

Question

for a school project I have to write a paper about the SPARK programming language, which I did, however part of it is writing a short program that takes an integer n and outputs the sum of squares from 1 to n. In C++ the program would look something like this:

#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;
} 

I am not familiar with SPARK at all, I found a similar program in Ada and modified it slightly, so it would work with integers instead of doubles and would output the result (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;

Now the question is how to make this Ada program into a SPARK one. I tried changing Ada.Text_IO to Spark_IO, but the IDE (GPS) gives me "file spark_io.ads" not found." Also the program should work with an arbitrary integer n, not just with 5, as in the example. Any help would be much appreciated.

Answer 1

I assume you are using GNAT SPARK 2014 for your example program. Your example program is already a valid SPARK program.

You could change the Sum_Of_Squares function to the code below to calculate the sum of an arbitrary integer that is read in on the console. It is not necessary to use an array to loop over. I changed the Integer to Natural, because I assumed you are only interested in the squares of numbers greater or equal to 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;

However, one of the advantages of SPARK is to add some extra information to allow automatic prove of defined properties of your program.

Hope that helped.