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 (+=, ...)
18 lines
262 B
Python
18 lines
262 B
Python
|
|
print("somme des n premiers entiers")
|
|
|
|
n = int(input("entrez n : "))
|
|
#@ assume n >= 0
|
|
|
|
s = 0
|
|
k = 0
|
|
while k <= n:
|
|
#@ invariant k <= n+1
|
|
#@ invariant s == (k - 1) * k // 2
|
|
#@ variant n - k
|
|
s += k
|
|
k += 1
|
|
|
|
print(s)
|
|
#@ assert s == n * (n+1) // 2
|