最大公約數 - 前後條件

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)