Skip to content

Instantly share code, notes, and snippets.

@wenjianhn

wenjianhn/GCD.tla

Created June 26, 2015 04:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save wenjianhn/4a0551bafe954c6a7f46 to your computer and use it in GitHub Desktop.
Save wenjianhn/4a0551bafe954c6a7f46 to your computer and use it in GitHub Desktop.
Download ZIP
The Greatest Common Divisor
Raw
GCD.tla
-------------------------------- MODULE GCD --------------------------------
EXTENDS Integers
Divides(p, n) ==
\E q \in -n..n : n = q * p
DivisorsOf(n) == {p \in -n..n : Divides(p, n)}
SetMax(S) ==
CHOOSE i \in S : \A j \in S : i >= j
GCD(m, n) ==
SetMax(DivisorsOf(m) \cap DivisorsOf(n))
=============================================================================
\* Modification History
\* Last modified Fri Jun 26 11:17:37 CST 2015 by jian
\* Created Fri Jun 26 11:14:28 CST 2015 by jian
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment