My immediate observation was simply that if end < begin then the loop will possibly never terminate, or might terminate after consuming all memory iff the point

My immediate observation was simply that if end < begin then the loop will possibly never terminate, or might terminate after consuming all memory iff the pointer eventually overflows to zero and doesn't cause a null pointer exception in the process. That could be fixed with a guard of course; it just happens that the program as given doesn't have one. (that's essentially the same point as your example showing referencing elements in the wrong order; it also does not address the question of whether the pointers are even in the same logical array or not). Still, apart from that, it's a nice article that succinctly explains a concept in an area where I find most of the literature tends to be somewhat intractable (formal methods). I say this as someone who's had a lot of interest in the topic for many years, but no background in it, so my knowledge is mostly limited to the contents of articles like this one. I do however really like the idea of using axioms and invariants in place of runtime assertions as a way to prove correctness of certain parts of applications. I think in combination with higher level unit & system tests we could have get a fairly practical system of showing both the correctness and applicability of solutions (as there's no point in having a system that is provably correct but solves the wrong problem). It's something I plan to get around to working on some day.