mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
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
|