On Wednesday, 6 August 2014 at 17:03:44 UTC, Marc Schütz wrote:
I guess we're talking past each other. You were saying that Hoare logic doesn't work with non-terminating loops, and I was responding that there was no non-terminating loop in the example. That's all there is to it.
Oh well, but a terminating loop that does not change the condition is just an empty statement. So then you have basically proved that it isn't a loop… ;)
