The loop invariant is obvious. The "decreases" annotation tells the compiler that a variable gets smaller (can often be inferred); clearly "increases" would be a desirable form of annotation as well. Both of these could be covered by marks instead of requiring key words in the language.
Consider this snippet of Dafny code from http://rise4fun.com/Dafny/tutorial/guide:
The loop invariant is obvious. The "decreases" annotation tells the compiler that a variable gets smaller (can often be inferred); clearly "increases" would be a desirable form of annotation as well. Both of these could be covered by marks instead of requiring key words in the language.