最大公约数 - 前后条件

Question

以下为gcd方法提供了前后条件。

pre: x > 0 & y > 0 
post: result > 0 & 
     x mod result = 0 & y mod result = 0 & 
     ∀t:Integer · t > 0 & x mod t = 0 & y mod t = 0 ⇒ result mod t = 0 

不过，我有以下职位条件的麻烦......对我来说，基本上是说发现任何整数，它是由两个整除。它如何得到最大的除数，实际上说的条件是什么？

Answer 1

这一个确保result是最大的所有公约数。

∀t:Integer·t>0 & x mod t=0 & y mod t = 0 ⇒ result mod t = 0 

它说，任何t，这是x和y一个最大公约数，也是result

编辑的因子：你应该看了上面的一行：

∀t:Integer·((t>0 & x mod t=0 & y mod t = 0) ⇒ result mod t = 0)