java - 最大公約数 - 事前条件と事後条件

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の公約数であるanyはの約数でもあるxyresult

編集: 上記の行を次のように読む必要があります。

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