src/HOL/SPARK/Manual/document/Gcd.adb
author nipkow
Tue, 17 Jun 2025 14:11:40 +0200
changeset 82733 8b537e1af2ec
parent 45044 2fae15f8984d
permissions -rw-r--r--
reinstated intersection of lists as inter_list_set

package body Greatest_Common_Divisor
is

   procedure G_C_D(M, N: in Natural; G: out Natural)
   is
      C, D, R: Integer;
   begin
      C := M; D := N;
      while D /= 0 loop
         --# assert C >= 0 and D > 0 and Gcd(C, D) = Gcd(M, N);
         R := C rem D;
         C := D; D := R;
      end loop;
      G := C;
   end G_C_D;

end Greatest_Common_Divisor;