Greatest common divisor: Difference between revisions
Content deleted Content added
Line 599:
Here is an implementation of Stein’s algorithm, without proofs of termination or correctness.
<
(*
Line 802:
end
(********************************************************************)</
Line 809:
Here is an implementation of Stein’s algorithm, this time with a proof of termination. Notice that the proof is rather ‘informal’; this is practical systems programming, not an exercise in mathematical logic.
<
(*
Line 1,027:
end
(********************************************************************)</
===Euclid’s algorithm, with proof of termination and correctness===
Line 1,033:
Here is an implementation of Euclid’s algorithm, with a proof of correctness.
<
(*
Line 1,263:
end
(********************************************************************)</
===Some proofs about the gcd===
Line 1,270:
For the sake of interest, here is some use of ATS's "props"-based proof system. There is no executable code in the following.
<
(* Definition of the gcd by Euclid’s algorithm, using subtractions;
Line 1,402:
else
gcd_isfun__nat_nat__ (pfd, pfe)
end</
=={{header|AutoHotkey}}==
|