Greatest common divisor: Difference between revisions
m
→Euclid’s algorithm, with proof of termination and correctness
m (→{{header|ATS}}) |
|||
Line 1,036:
(*
GCD of two integers, by
Compile with ‘patscc -o gcd gcd.dats’.
Line 1,104:
(* *)
(*
unsigned integers. *)
extern fun {tk : tkind}
g1uint_gcd_euclid :
{u, v : int}
(g1uint (tk, u),
Line 1,113:
g1uint (tk, gcd (u, v))
(*
signed integers, giving an unsigned result. *)
extern fun {tk_signed, tk_unsigned : tkind}
g1int_gcd_euclid :
{u, v : int}
(g1int (tk_signed, u),
Line 1,122:
g1uint (tk_unsigned, gcd (u, v))
(* Let us call these functions
overload
overload
overload gcd with
(********************************************************************)
Line 1,149:
implement {tk}
let
(* The static variable v, which is defined within the curly
Line 1,220:
implement {tk_signed, tk_unsigned}
let
(* Prove that gcd(abs u, abs v) equals gcd(u, v). *)
Line 1,227:
(* Compute gcd(abs u, abs v). The ‘g1i2u’ notations cast the
values from signed integers to unsigned integers. *)
end
Line 1,264:
(********************************************************************)</lang>
===Some proofs about the gcd===
| |||