Three Dollar Quill

Okay, still getting to grips with Dafny. It's not a fast process when I'm just doing a little a day, I guess. In any case, I now understand something that had me a little confused. The meaning of the keywords kind of changed around between Dafny 3 and 4, and a lot of the stuff I'm reading happens to be for 3, but I'm using 4 because I wanted to make some use of the standard library.

In particular, what 3 expresses via function method is just function in 4, while what 3 calls function is ghost function in 4.

In light of this, I've slightly updated my existing files to make sure that they're actually expressing what they're supposed to; basically just making sure that the recurrent forms are ghost functions.

I also ran across some documentation about telling Dafny to generate counterexamples; I'll have to try that out later.

Aside from that, I tried to put together some flexibly generic code for summing over sets, using a short guide I found about iterating over a collection, and I'm not sure what I'm doing wrong, but my attempts to follow the directions seem to be putting Dafny in another infinite loop, so that'll be some kind of pain to troubleshoot.

(At least the infinite version should be "easier", since I think that has to be ghost.)

Also, thinking about this, I'm going to have to remember how to rigorously prove convergence, and that could be... a thing.

I may end up needing to take a break from this and focus on somewhat less intimidating pursuits. For the moment, I should get ready for bed.

Good night.