#### Topic: Dafny the proof of sorting by a choice.

//the Predicate which states that a segment [begin. end) it is sorted. predicate SortedRange (a: array <int>, begin: int, end: int) requires a! = null; requires 0 <= begin <= end <= a. Length; reads a; {forall i, j:: begin <= i <j <end ==> a [i] <= a [j]}//the Predicate which states that function rearranges in places array cells [begin. end)//also does not change a remaining array predicate PremutateRange (a: seq <int>, b: seq <int>, begin: int, end: int) requires |a | == |b |; requires 0 <= begin <= end <= |a |; {(forall i:: 0 <= i <begin && end <= i <|a | ==> a [i] == b [i]) && multiset (a [begin. end]) == multiset (b [begin. end]) && multiset (a) == multiset (b) && a [0. begin] == b [0. begin] && a [end. |a |] == b [end. |a |]} method MinIndex (a: array <int>, begin: int, end: int) returns //a precondition guaranteeing that a segment [begin. end) not the empty. requires 0 <= begin <end <= a. Length; ensures begin <= index <end;//a postcondition guaranteeing that the index of a minimum element is returned. ensures forall t:: begin <= t <end ==> a [t]> = a [index];//a postcondition guaranteeing that the index of the first of identical elements is returned. ensures forall t:: begin <= t <index ==> a [t]! = a [index]; {index: = begin; var i: = begin + 1; while i <end invariant begin <= index <i <= end; invariant forall t:: begin <= t <i ==> a [t]> = a [index]; invariant forall t:: begin <= t <index ==> a [t]! = a [index]; {if a [index]> a [i] {index: = i;} i: = i + 1;}} method SelectionSortRange (a: array <int>, begin: int, end: int) requires a! = null; requires 0 <= begin <= end <= a. Length; modifies a; ensures SortedRange (a, begin, end);//old (a [.] ) Does a copy of an array which was on an input in function//if to write old (a) that we receive the link to an array//as the link did not change, the postcondition becomes senseless ensures PremutateRange (a [.], old (a [.]), begin, end); {if end - begin <= 1 {// without helps understands that arrays from 0 or 1 elements are sorted. return;} var i: = begin; while i <end - 1 invariant begin <= i <end; invariant forall lo, hi:: begin <= lo <i && i <= hi <end ==> a [lo] <= a [hi]; invariant SortedRange (a, begin, i); invariant PremutateRange (a [.], old (a [.]), begin, end); {var min: = MinIndex (a, i, end); a [i], a [min]: = a [min], a [i]; i: = i + 1;} } As a whole impressions from rather pleasant. Directions the perspective. But a piece very crude. Error messages are worse, than at With ++. To understand that not all clearly is necessary it . Only so it is possible to localize and understand a problem.... <<RSDN@Home 1.2.0 alpha 5 rev. 62>>