9 ms·
From what I remember, the assignment was to write a function that implemented quick sort (or something else moderately complex) and getting it to run and satisf
by seibelj 10y ago
From what I remember, the assignment was to write a function that implemented quick sort (or something else moderately complex) and getting it to run and satisfy the proof checker was exhausting.
Edit: Found a forum post I made during it asking for help. Oh, the frustrating memories... https://dafny.codeplex.com/discussions/546995 https://dafny.codeplex.com/discussions/546995
- pierrec 10y agoWow, the feedback you got on that forum has a pretty rare level of detail and helpfulness. Confusing syntax, perhaps, but the community is point for sure!
- harpocrates 10y agoI see. Googled the for Dafny quick sort and it does have some pretty long invariants. [1]: http://rise4fun.com/Dafny/ks http://rise4fun.com/Dafny/ks
- archgoon 10y agoDoes Dafny not provide any macros for their invariants declarations ensures clauses? The QuickSort Example has a lot of the same invariants again and again, and most of them boil down to "I swear that the integer values are valid indices into the array".
- houli 10y agoYes, you can define predicates that take parameters and use them as the invariants