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
.
- Am I misreading the error report?
- How does SPARK come up with this value of
R
?
- 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.
10 posts - 3 participants
Read full topic