SPARK Example

```
-------------------------------------------
-- double.ads (specification)
-------------------------------------------
package double
    with SPARK_Mode => On
is
    type SomeArrayType is array (Positive range <>) of Natural;

    function doubleArray(arr : in SomeArrayType) return SomeArrayType
        with
            Global => null,
            Depends => (doubleArray'Result => arr),
            -- set arbitrary range here in precondition to avoid overflow
            Pre => (for all idx in arr'Range => arr(idx) in 0..20000),
            -- prove that everything in the return array is even
            Post => (for all idx in arr'Range =>
                     isEven(doubleArray'Result(idx)));

    function isEven(num : in Natural) return Boolean with
             Contract_Cases =>
                 (num rem 2 = 0 => isEven'Result = True,
                  num rem 2 /= 0 => isEven'Result = False);

end double;

-------------------------------------------
-- double.adb (implementation)
-------------------------------------------
package body double is

    function doubleArray(arr : in SomeArrayType) return SomeArrayType with
        SPARK_Mode => On
    is
        doubled : SomeArrayType(arr'Range) := (others => 0);
    begin
        for i in arr'Range loop
            doubled(i) := 2 * arr(i);

            pragma Loop_Invariant(for all j in arr'First .. i =>
               doubled(j) = 2 * arr(j));
        end loop;

        return doubled;
    end doubleArray;


    function isEven(num : in Natural) return Boolean with
        SPARK_Mode => On
    is
    begin
        if num rem 2 = 0 then
            return True;
        else
            return False;
        end if;
    end isEven;
end double;

-------------------------------------------
-- main.adb
-------------------------------------------

with Ada.Text_IO;
with double; use double;

procedure Main
    with SPARK_Mode => On
is
    arr : SomeArrayType := (3, 7, 8, 0, 1);
    result : SomeArrayType := doubleArray(arr);
begin
     for i in result'Range loop
        Ada.Text_IO.Put(Integer'Image(result(i)) & ", ");
    end loop;
end Main;
```