2 ms·
I think even your example is not actually proving GCD, just that the result is _a_ common divisor. E.g. it would succeed if GCD(a, b) = 1 for all a, b.
by jcparkyn 3y ago
I think even your example is not actually proving GCD, just that the result is _a_ common divisor. E.g. it would succeed if GCD(a, b) = 1 for all a, b.
- contravariant 3y agoIt would, but combined with the postcondition you then get gcd(a,b) = ax + by = 1, which shows the gcd is indeed 1.