Hacker News Reader

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

View on HN

Wow, 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!

I see. Googled the for Dafny quick sort and it does have some pretty long invariants.

[1]: http://rise4fun.com/Dafny/ks

Does 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".

Yes, you can define predicates that take parameters and use them as the invariants

Reply on news.ycombinator.com