1

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

2

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

3

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

4

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

5

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.

6

Re: Dafny the proof of sorting by a choice.

Hello, Code Digger, you wrote: CD> Allow to disagree - a direction unpromising. Allow disagrees with disagreement. CD> And so, inside (at AutoProof it is exact, is assured that at "Dafny" too - see why) all CDs> is led ("the functional representation" (in sense of the functional CD> programming) with pure functions and explicit transmission of a state is broadcast. These are implementation details. CD> though it is not intended and cannot execute any code - only to specify and verify, it is enough of It. CD> therefore there the "strange" semantics if-then-else, for example), And what there the strange? CD> but global shared mutable state in it is not present.> Because - a surprise, a surprise - about it something is very difficult to prove CD. The global state generally is harmful. For about it not only it is difficult to prove something. But also about it it is difficult to person to understand something. It is a lot of problems more shortly, and advantages any. So even if to forget about verification I consider that the global state generally needs to be forbidden. CD> Because in such type over them to lead reasoning much easier! And how you without it generally are going to prove something? CD> Besides for the majority of them in Boogie and Z3 is available the 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. And what for? CDs> By the way, in the majority of these projects are not considered in any way and effects IO are not restricted, exceptions, etc. Dafna is able to work with the infinite sequences. For IO it is enough of it. As to exceptions that it is just necessary to divide functions on what never throw exceptions. And functions which are explicitly marked that throw exceptions. http://joeduffyblog.com/2016/02/07/the-error-model/ generally all blog I advise. There it is a lot of interesting. About all that in article is called abandonment will be caught by the verifier at a compilation stage.//Can throw exceptions int Foo () throws {...}//Never throws exceptions int Bar () {...}//We do not intercept an exception//So this function too should throw an exception int Baz () throws {//explicitly we say that Foo to throw an exception//It can is possible and is not explicit. Simply looking at the function signature//But in conditions when the absolute minority of functions can throw an exception//such approach much better//for at once it is visible where there can be a regional ohm. int value1 = try Foo ();//Bar an exception does not throw. int value2 = Bar (); return value1 + value2;} and at level of the verifier at us something turns out type such variant Result <T> {| Value {value: T} | Error {ex: Exception}} Result <int> Baz () {int value1 = match (Foo ()) {| Vlaue (v) => v | Error as error => return error;} int value2 = Bar (); return Result. Value (value1 + value2);} CD> Also is all only for one-continuous programming - without everyone concurrency, races or synchronization! And the multithreading on divided storage in the application-oriented code is precisely necessary? For muzhiks in MSR managed to write the whole OS without a global state and a multithreading on divided storage. CD> Personally at me arises a question: if the functional programming "inside" is all the same used why not to use it "outside"? On that that productivity and storage consumption in real applications have solving value. And with the imperative code by these indexes  generally cannot compete. Often problems begin already with  computing complexity of the functional decision. CD> 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", its "representation" and "engine" coincide. In case of the big rupture between imperative "the objective language" and the "functional" internal representation it becomes almost impossible. I think, it is a question of tools. For example, very strongly facilitate life generation of the data on which can restrictions are not fulfilled. Then there should be a possibility to launch function with this data under a debugger.... <<RSDN@Home 1.2.0 alpha 5 rev. 62>>