#### 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>>

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

Hello, WolfHound, you wrote: WH> to understand that not all clearly is necessary it  . WH> Only so it is possible to localize and understand a problem. +1 to a heap my last year's approach to a shell with sorting on Dafne: http://thedeemon.livejournal.com/107067.html

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

Hello, D. Mon, you wrote: DM> To a heap my last year's approach to a shell with sorting on Dafne: DM> http://thedeemon.livejournal.com/107067.html At you there a heap of bugs. On it: predicate pairwiseOrdered (a: array, n: int) requires a! = null; requires n <= a. Length; reads a; {forall i:: 0 <= i <n-1 ==> a [i] <= a [i+1]} it is received stdin.dfy (6,36): Error: arguments to <= must be of a numeric type, char, or a collection type (instead got _T0) 1 resolution/type errors detected in stdin.dfy If to add type to an array it is received: stdin.dfy (6,2): Warning: Selected triggers: {a [i]} (may loop with "a [i + 1]")/! \Suppressing loops would leave this expression without triggers. And this "warning" kills  on a root. It generally ceases to check something. It is possible to correct so: predicate pairwiseOrdered (a: array <int>, n: int) requires a! = null; requires n <= a. Length; reads a; {forall i, j:: : j == i + 1 ==> (0 <= i <n - 1 ==> a [i] <= a [j])} Why at  does not suffice brains on this transformation There and then even it is not necessary to think. Here the corrected version of your decision. Plus the proof of that that a resultant array is swap initial. http://rise4fun.com/Dafny/LtfB pay attention to call PremutateRange (a [.], old (a [.]), 0, a. Length); old (a) does not work, for returns not an array copy, and a copy of the link to an array. And the predicate starts to compare an array to itself, instead of with the old version.... <<RSDN@Home 1.2.0 alpha 5 rev. 62>>

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

Hello, WolfHound, you wrote: WH> At you there a heap of bugs. It at posting <int> in places were ate, did not follow. The Original without bugs was, was compiled. Here the full text: https://gist.github.com/thedeemon/ef85d … db5eb44ef4

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

Hello, WolfHound, you wrote: WH> As a whole impressions from  rather pleasant. Directions the perspective. WH> but a piece very crude. Error messages are worse, than at With ++. WH> to understand that not all clearly is necessary it  . WH> Only so it is possible to localize and understand a problem. Allow to disagree - a direction unpromising. About "Dafnu" I know, probably, half a year, studied  or that there was. Saw one more language on the same subject from MSR, even it is more interesting, but forgot a title. I have some  to development AutoProof - static  for language Eiffel. In general, I worked with such pieces as "Dafna" a little and I represent internal "kitchen". And so, inside (at AutoProof it is exact, it is assured that at "Dafny" too - see why) all is led (is broadcast) "the functional representation" (in sense of the functional programming) with pure functions and explicit transmission of a state. It is connected to that, as AutoProof (i.e. Eiffel), and "Dafna" (AFAIR)  in a special intermediate language for verification - Boogie (which it is then broadcast in SMT-konstrejnty and is processed Z3). In Boogie there are preconditions and postconditions (well, it is a lot of that there is though it is not intended and cannot execute any code - only to specify and verify, therefore there the "strange" semantics if-then-else, for example), but global shared mutable state in it are not present. Because - - about it something is very difficult to prove a surprise, a surprise. So all object-oriented, imperative, stateful programs at translation turn to a scattering of the functions evidently modifying "a global state", presented by the hash table which it on-essence and is (actually not the hash table, and display - map - from lines in values; as Boogie the code is not fulfilled by physical implementation of such display to it is absolutely not necessary). But actually the need for pure functions on it does not come to an end. It appears that semantics of a considerable quantity of fundamental concepts - such as Set, Sequence, Map etc. - most easier to express in the form of "pure" (mathematical) operations over them (such which accept old object and return new) as it becomes in the mathematician, the logician or formalism Abstract Data Types. Because in such type over them to lead reasoning much easier! Besides for the majority of them in Boogie and Z3 there is a built in support. And "composite" semantics though same hash table to express without usage of concepts Sequence and Set - in one only operational terms - it is difficult enough. And to prove - it is even more difficult. By the way, in the majority of these projects are not considered in any way and effects IO are not restricted, exceptions, etc. And it is all only for one-continuous programming - without everyone concurrency, races or synchronization! Personally I have a question: If the functional programming "inside" is all the same used why not to use it "outside"? To understand error messages from the verifier all the same it is necessary to understand internal model, and it - functional. Without understanding of model it will be impossible to make something when "the ends" proofs did not converge and it is necessary to strengthen the specification or to add a lemma." To guess "the correct lemma happens very uneasy even in case of operation to the formal logic when"language", it" representation "and" an engine "coincide. In case of the big rupture between imperative" the objective language "and" functional "internal representation it becomes almost impossible. About it I invented" conservation law PhD ": or to you is necessary PhD to write on language for correct-by-construction programming, or it is required to you for the proof of a correctness of programs in"normal"language.:-D so personally I study Isabelle and Idris. Still F* (F-star) from MSR - very interesting project. About the same implement in Liquid Haskell.