Играюсь вот с этой штукой:
http://research.microsoft.com/en-us/projects/dafny/
Попробовать в браузере можно тут:
http://rise4fun.com/dafny/Hello

Вот в этом коде дафна не может доказать первый ассерт. Но с моей точки зрения должна.
Это баг или я что-то не понимаю?

lemma TestMultiset(a : array<int>, begin : int, mid : int, end : int)
  requires a != null;
  requires 0 <= begin <= mid <= end <= a.Length;
{
  assert multiset(a[begin..mid]) + multiset(a[mid..end]) == multiset(a[begin..end]);
  assert a[begin..mid] + a[mid..end] == a[begin..end];
  assert |multiset(a[begin..mid])| + |multiset(a[mid..end])| == |multiset(a[begin..end])|;
  assert |a[begin..mid]| + |a[mid..end]| == |a[begin..end]|;
}

Без этого у меня квиксорт доказать не получается.