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);