Наибольший общий делитель — предварительные и постусловия

Ниже приведены предварительные и последующие условия для метода 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

Тем не менее, у меня возникли проблемы с выполнением условия публикации... для меня это в основном говорит, что нужно найти любое целое число, которое делится на оба. Как он получает максимальный делитель, о чем на самом деле говорят условия?


java uml preconditions post-conditions
person mark    schedule 29.12.2012    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Это гарантирует, что 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)
person gefei    schedule 29.12.2012