Wiki page on Dynamic Frames

[samuelgruetter]

I was struggling to understand how to get modifies clauses right. If I understand correctly, there's a mechanical pattern involving Repr and Valid, which is just some boilerplate code I have to write and then not worry about it anymore, or which I could even have autogenerated by :autocontracts. Is there a guide about this? At the moment, all I have is

• the section about :autocontracts in DafnyRef.pdf
• Chapter 9 in http://leino.science/papers/krml221.pdf

What's missing is a bigger example with at least three layers of nested objects and some while loops, because that's where the difficulties usually come up.

The revisions of this gist show how I got stuck on a modifies clause problem and then solved it.
Not sure if I would have succeeded without talking to @RustanLeino, so the issue is "create documentation so that users can learn this on their own".

[robin-aws]

This might be at least a partial solution: dafny-lang/libraries#22