가장 큰 일반 제수 - 사전 조건과 사후 조건

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 

이 x 및 y의 공약수가 어떤 t는, result

편집의 제수는 것을 말한다 :

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