3 ms·
I 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
by harpocrates 10y ago
I 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