# Two SPARK questions

To help learn me some SPARK, I decided to try implementing the Euclidean Algorithm. With a generic type. Basically (simplified from what I actually have, which includes contracts):

``````generic

type Ring_Element is private;

Zero : Ring_Element;

with function "=" (Left, Right : Ring_Element) return Boolean is <>;
with function Size (Value : Ring_Element) return Natural;
with function "-" ( Left, Right : Ring_Element ) return Ring_Element is <>;
with function "rem"
(Dividend, Divisor : Ring_Element) return Ring_Element is <>;
package Euclidean is ...
``````

And the body Euclidean:

``````    function Gcd ( A, B : Ring_Element ) return Ring_Element is

M: Ring_Element := A;
N: Ring_Element := B;

begin

while N /= Zero loop

declare
R : constant Ring_Element := M rem N;
begin
M := N;
N := R;
end;

end loop;

end Gcd;
``````

The algorithm has several nice properties. One is a loop invariant that r divides a - b.

I’ve struggled with getting SPARK to accept a contract to that effect. My latest iteration has this:

``````   if R /= Zero then ( A rem R ) - ( B rem R ) = Zero
``````

…but when I instantiate `Ring_Element => Integer` it reports

``````   euclidean.adb:26:41: medium: loop invariant might fail in first iteration, cannot prove (A rem R ) - ( B rem R ) = Zero, in instantiation at main.adb:32 (e.g. when A = -2 and B = 1 and M = 1 and R = 3)[#0]
``````

That… makes no sense. It’s not possible for the algorithm to start with those inputs and end up with `R = 3`.

1. Am I misreading the error report?
2. How does SPARK come up with this value of `R`?
3. Any advice on writing a contract for this condition? I’ve generally had trouble with guaranteeing arithmetic expressions like `A + B` and `A - B`; I understand why, but am not sure how to handle them. Using `rem R` was something I thought might help here, it did get me past the under/overflow, and it is also true.

Your function has no return statement, so it is illegal Ada and SPARK. It also has no `pragma Loop_Invariant`, so clearly this is not what you’re trying to prove. Please give us the entire spec of `Euclidean`, especially the declaration of `Gcd` with its contract, and the actual body of `Gcd` that you’re trying to prove, along with the instantiation of Euclidean that is being proved, including any declarations used by that instantiation.

SPARK’s counterexamples are often impossible, and it seems that this reflects the prover not using all the information that is available. Those who are proficient at SPARK seem to have learned what these limitations are and how to write predicates that work around them. Sometimes avoiding conditional expressions seems to help:

`(R = Zero or else A rem R = B rem R)`

Thank you for the thoughts!

Sorry, I was cut-and-paste-in various parts and missed that. In fact the original source code has a comment to that effect (you’ll see below) because I wanted to highlight that. (I once had a devil of a time debugging a C++ program where I’d forgotten a return statement.)

I was deliberately excluding them from the basic listing, but I’ll include them below.

Replacing it with your suggestion didn’t help.

ok

Some comments will reflect the fact that it was passing proofs until I added the postcondition in question (gcd must divide a - b).

### spec

``````-- @summary a generic package with a generic function to compute a gcd
-- of two elements of a Euclidean Ring
--
-- @description
-- This package implements the Euclidean Algorithm for a generic,
-- user-specified Euclidean Ring.
-- The main purpose is to demonstrate how SPARK 2014 can prove its correctness.
-- The main feature is the Gcd function, which returns a greatest common divisor
-- (gcd) of its inputs.
--
-- @generics
-- - Ring_Element
--   specifies the type of objects for which we want to compute gcd's;
--   algebraically speaking, this should be a Euclidean Ring.
-- - "="
--   a function that returns @code True iff its two parameters are equivalent
--   in the given @code Ring_Element
-- - Size
--   a function that takes a @code Ring_Element as a parameter
--   and returns an integer result that in some way measures @code Value's size
-- - Zero
--   a @code Ring_Element that serves as an additive identity; i.e., 0
-- - "rem"
--   a function that accepts two nonzero @code Ring_Elements' parameters and returns
--   either @code Zero or
--   another @code Ring_Element whose @code Size is no larger than the parameters'
generic

type Ring_Element is private;
-- specifies the type of objects for which we want to compute gcd's;
-- algebraically speaking, this should be a Euclidean Ring.

Zero : Ring_Element;
-- needs to be the ring's additive identity

with function "=" (Left, Right : Ring_Element) return Boolean is <>;
-- should returns True iff Left and Right have the same value.
-- @param Left a ring element to compare
-- @param Right a ring element to compare
-- @return whether Left and Right are equal

with function Size (Value : Ring_Element) return Natural with
Pre => Value /= Zero;
-- with the integers it is customary to use `abs`
-- @param Value a ring element whose size we want
-- @return the size of Value

with function "-" ( Left, Right : Ring_Element ) return Ring_Element is <>;

with function "rem"
(Dividend, Divisor : Ring_Element) return Ring_Element is <> with
Pre  => Divisor /= Zero,
Post =>
("rem"'Result = Zero
or else
(Size ("rem"'Result) < Size (Divisor)
and then Size ("rem"'Result) <= Size (Dividend)));
-- to guarantee termination, the result should be "smaller" than Divisor.
-- how precisely this is accomplished can depend on the ring,
-- and need not be specified.
-- @return the remainder of dividing the Dividend by the Divisor

package Euclidean is

function Gcd (A, B : Ring_Element) return Ring_Element with
Pre  => (A /= Zero and then B /= Zero and then Size (B) < Size (A)),
Post =>
(Gcd'Result /= Zero and then Size (Gcd'Result) <= Size (A)
and then Size (Gcd'Result) <= Size (B)
and then ( A rem Gcd'Result ) - ( B rem Gcd'Result ) = Zero
);
-- @return a greatest common divisor (gcd) of A and B
-- @param A nonzero ring element
-- @param B nonzero ring element

end Euclidean;
``````

### body

``````package body Euclidean is

function Gcd (A, B : Ring_Element) return Ring_Element is

-- initialize local variables
M : Ring_Element := A;
N : Ring_Element := B;

begin

-- loop until the smaller is zero
while N /= Zero loop

declare
R : constant Ring_Element := M rem N;
begin
M := N;
N := R;
pragma Loop_Invariant
((M /= Zero and then Size (M) <= Size (A)
and then Size (M) <= Size (B))
and then
(N = Zero
or else (Size (N) <= Size (A) and then Size (N) <= Size (B)))
and then
( if R /= Zero then ( A rem R ) - ( B rem R ) = Zero )
);
end;

end loop;

-- the compiler will give an error if the following statement is missing
return M;

end Gcd;

end Euclidean;
``````

### instantiation

``````   function Integer_Size (Value : Integer) return Integer is (abs (Value)) with
Pre => Value > Integer'First;

subtype Good_Integer is Integer range Integer'First + 1 .. Integer'Last;
-- must start at Integer'First + 1, otherwise
-- proof fails on instantiation, likely because
-- abs ( Integer'First ) overflows

package Euclidean_ZZ is new Euclidean
(Ring_Element => Good_Integer, Zero => 0, Size => Integer_Size);
``````

I must have misunderstood something:

``````euclidean.ads:43:08: error: incorrect placement of aspect "Pre"
43 |       Pre => Value /= Zero;
|       ^~~~~~~~~~~~~~~~~~~~

euclidean.ads:52:08: error: incorrect placement of aspect "Pre"
52 |       Pre  => Divisor /= Zero,
|       ^~~~~~~~~~~~~~~~~~~~~~~

euclidean.ads:53:08: error: incorrect placement of aspect "Post"
53>|       Post =>
... | ...
57 |               and then Size ("rem"'Result) <= Size (Dividend)));
``````

GCC 13.1.0 makes the same complaints.

AFAICT, it should be impossible to prove `Gcd` correct for `Integer` because it is incorrect. Given the definition of `"rem"` for `Integer` [ARM 4.5.5(27-30)], `Gcd (-14, 6) = -2` and `Gcd (-14, -6) = -2`. Since 2 is a common divisor of these pairs and 2 is greater than -2, your definition does not work for negative `A`.

I copied & pasted that and the gnat compiler I had wasn’t complaining about that… is that not where it’s supposed to go?

Maybe I misunderstand you, but negative gcd is allowed in algebra. (As opposed to arithmetic.) The definition is that g is a gcd of a, b if any d that divides both a and b also divides g. Since -2 divides 2 and 2 divides -2, they are both gcd’s from that point of view. (this is a bigger deal when it comes to polynomials)

From the arithmetic point of view, of course, only 2 is “the” gcd.

But I think I misunderstand what you’re saying, so if you mean that something in the contracts is implying the result has to be greater than `Zero`, I’ve missed it so far.

Ada-12 allows aspects on generic formal subprograms, but states that there are no language-defined aspects that may be used for them. ISO/IEC 8652:2023 allows the `Pre` and `Post` aspects on generic formal subprograms.

I guess I’m only familiar with the arithmetic definition of GCD, so you should probably ignore my comment. I noticed that your GCD allowed negative operands, which I’d not encountered before, and used `"rem"` for the remainder. Knowing that `"rem"` has interesting results for negative operands, I looked at what your instance would do for negative values, and got results that are incorrect for my understanding of GCD and went off half cocked.

The math you’re using is also probably why your postcondition isn’t what I’d expect.

Yes. For the compiler, you can say `-gnat2022` on the command line, but for gnatprove it has to be in the project.