mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
53 lines
1.1 KiB
Python
53 lines
1.1 KiB
Python
|
###################################################
|
||
|
|
# ...[expr] += ... #
|
||
|
|
###################################################
|
||
|
|
|
||
|
|
def side_effect1(tab):
|
||
|
|
#@ ensures result == 0
|
||
|
|
#@ ensures len(tab) == len(old(tab)) + 1
|
||
|
|
tab.append(1)
|
||
|
|
return 0
|
||
|
|
|
||
|
|
a = [0]
|
||
|
|
tab = []
|
||
|
|
|
||
|
|
a[side_effect1(tab)] += 1
|
||
|
|
|
||
|
|
#@ assert a[0] == 1
|
||
|
|
#@ assert len(tab) == 1
|
||
|
|
|
||
|
|
|
||
|
|
###################################################
|
||
|
|
# expr[...] += ... #
|
||
|
|
###################################################
|
||
|
|
|
||
|
|
def side_effect2(tab):
|
||
|
|
#@ ensures result[0] == 0
|
||
|
|
#@ ensures len(result) == 1
|
||
|
|
#@ ensures len(tab) == len(old(tab)) + 1
|
||
|
|
tab.append(1)
|
||
|
|
return [0]
|
||
|
|
|
||
|
|
tab.clear()
|
||
|
|
|
||
|
|
side_effect2(tab)[0] += 1
|
||
|
|
|
||
|
|
#@ assert len(tab) == 1
|
||
|
|
|
||
|
|
|
||
|
|
###################################################
|
||
|
|
# expr[:] #
|
||
|
|
###################################################
|
||
|
|
|
||
|
|
def side_effect3(tab):
|
||
|
|
#@ ensures len(result) == 3
|
||
|
|
#@ ensures len(tab) == len(old(tab)) + 1
|
||
|
|
tab.append(1)
|
||
|
|
return [0, 1, 2]
|
||
|
|
|
||
|
|
tab.clear()
|
||
|
|
|
||
|
|
side_effect3(tab)[:]
|
||
|
|
|
||
|
|
#@ assert len(tab) == 1
|