Interesting. There are certainly different kinds of assumptions and invariants. I like the idea of separating them by local vs. global scope; the latter are und

Interesting. There are certainly different kinds of assumptions and invariants. I like the idea of separating them by local vs. global scope; the latter are underdocumented. Much as I like, say, the javadoc format, it channels devs into "function by function" thinking and documentation, and global assumptions and global invariants, typically do not get treated adequately.