Meta:
What are the limitations on what Static_Predicate can verify? It seems like this could be quite powerful, but not as powerful as runtime checks, since not everything can be checked at compile time.
In Ada there is Dynamic_Predicate for the other cases :-)
Does the loop break if the invariant fails, or does it stop the program?
Ada has an elaborate infrastructure to allow you to choose how to react to failures, how to handle them, what failures to ignore, etc. At least, it stops the program.
I don't think this is quite as important, seeing as D has the pure keyword.
Purity means you can't use mutable values from outer scopes. The point of those Spark annotations (and @outer()) is to do the opposite: to specify the flow of information in system programming when you are not using purity.
Bye, bearophile
