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

【问题标题】：Greatest Common Divisor - Pre and Postconditions最大公约数 - 前置条件和后置条件
【发布时间】：2012-12-29 13:40:08
【问题描述】：

下面提供了 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

【解决方案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)

【讨论】：