#### Topic: Dafny, arrays and multisets

I am played here with this piece: http://research.microsoft.com/en-us/projects/dafny/ to Try in the browser it is possible here: http://rise4fun.com/dafny/Hello Here in this code cannot prove the first . But from my point of view should. It is a bug or I do not understand something? 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] |;} without it at me it is impossible to prove.... <<RSDN@Home 1.2.0 alpha 5 rev. 62>>