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 (+=, ...)
17 lines
236 B
Python
17 lines
236 B
Python
|
|
s = 0
|
|
|
|
for x in range(100, -1, -1):
|
|
#@ invariant s == 5050 - x*(x+1)//2
|
|
s = s + x
|
|
|
|
#@ assert s == 5050
|
|
|
|
s = 0
|
|
|
|
for x in range(1, 100, 2):
|
|
#@ invariant s == x'index * (2*x'index + 1)
|
|
s = s + x + x+1
|
|
|
|
#@ assert s == 5050
|