mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
21 lines
265 B
Python
21 lines
265 B
Python
|
|
a = input("entrez a : ")
|
|
b = input("entrez b : ")
|
|
|
|
#@ assume b >= 0
|
|
|
|
p = a
|
|
q = b
|
|
r = 0
|
|
while q > 0:
|
|
#@ invariant 0 <= q and r + p * q == a * b
|
|
#@ variant q
|
|
if q % 2 == 1:
|
|
r = r + p
|
|
p = p + p
|
|
q = q // 2
|
|
|
|
print(r)
|
|
#@ assert r == a * b
|
|
|