mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
23 lines
323 B
Python
23 lines
323 B
Python
|
|
s = 0
|
|
|
|
for i in range(100):
|
|
#@ invariant s == i
|
|
#@ invariant i < 11
|
|
if i == 10:
|
|
break
|
|
s += 1
|
|
|
|
#@ assert s == 10
|
|
|
|
s = 0
|
|
|
|
for i in range(100):
|
|
#@ invariant i <= 42 -> s == i*(i-1)//2
|
|
#@ invariant i > 42 -> s + 42 == i*(i-1)//2
|
|
if i == 42:
|
|
continue
|
|
s += i
|
|
|
|
#@ assert s == 4908
|