mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
3671864507
- New examples using the new syntax (+=, ...) - New examples using the new methods (.pop(), .append(), ...) - Update old examples with assignement operators (+=, ...)
13 lines
213 B
Python
13 lines
213 B
Python
|
|
def pgcd(a, b):
|
|
#@ requires a > 0 and b > 0
|
|
while a != b:
|
|
#@ invariant a > 0 and b > 0
|
|
#@ variant a + b
|
|
if a < b:
|
|
b -= a
|
|
else:
|
|
a -= b
|
|
return a
|
|
|