Здравствуйте, WolfHound, Вы писали:
WH>Вот в этом коде дафна не может доказать первый ассерт. Но с моей точки зрения должна.
WH>Это баг или я что-то не понимаю?
WH>WH>lemma TestMultiset(a : array<int>, begin : int, mid : int, end : int)
WH> requires a != null;
WH> requires 0 <= begin <= mid <= end <= a.Length;
WH>{
WH> assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);
WH> assert a[begin..mid] + a[mid..end] == a[begin..end];
WH> assert |multiset(a[begin..mid])| + |multiset(a[mid..end])| == |multiset(a[begin..end])|;
WH> assert |a[begin..mid]| + |a[mid..end]| == |a[begin..end]|;
WH>}
WH>
WH>Без этого у меня квиксорт доказать не получается.
А у тебя интервалы полуоткрытые или закрытые?
Для закрытых интервалов a[begin..mid] + a[mid..end] == a[begin..end] + a[mid], вообще-то.
Перекуём баги на фичи!
