最大公约数-前置和后置条件

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)