Coding 2024-01-24
Guys, it is really hard to write this stuff incrementally when I assume that "not filling in the branches of an if statement" will result in some kind of verification error, and instead it just makes my laptop fans try to launch it through the ceiling.
I've changed things up a bit:
- a ghost function to specify behavior; I think it assumes that Dafny's real type is associative and commutative under addition
- a ghost predicate for stating that a dyadic function acts as a total ordering
- a lemma stating that any finite set has a minimum according to a given total ordering
- a summation method that requires a total ordering to fix the order of execution
I am doing something wrong with the last bit, but I can't tell what.
...
A-ha! I neglected to invoke the lemma in the method, which caused Dafny to go into an infinite loop because I don't know!
A few more tweaks later, and now I just need to determine why Dafny appears to think that 0.0 might not be equal to 0.0.
...
I think I understand the gap between what I'm trying to get Dafny to accept and what it has available to work with, but I don't want to deal with it...
So I didn't. I stripped out the ghost function and made the "regular" function be the entire implementation. I'll try not to care about that too much.
Once I got the code all verifying, I figured out which asserts I could get rid of, which turns out to be risky because the ones I couldn't get rid of put it into an infinite loop again.
So, the code is, if not clean, at least sort of short. Maybe I'll clean it up later. Maybe I'll move on to other bits of code. Maybe I'll decide to do something else entirely.
I'll work that all out later, and for now get to bed, because sleepy.
Good night.