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 (+=, ...)
19 lines
293 B
Python
19 lines
293 B
Python
|
|
print("racine carrée entière")
|
|
|
|
n = int(input("entrez n : "))
|
|
#@ assume n >= 0
|
|
|
|
r = 0
|
|
s = 1
|
|
while s <= n:
|
|
#@ invariant 0 <= r
|
|
#@ invariant r * r <= n
|
|
#@ invariant s == (r+1) * (r+1)
|
|
#@ variant n - s
|
|
r += 1
|
|
s += 2 * r + 1
|
|
|
|
print(r)
|
|
#@ assert r*r <= n < (r+1)*(r+1)
|