[haimez]

How else do you "prove" trivial algorithms other than by removing the realities of an actual runtime environment?

I'm pretty sure you're right though. Integers must have been defined as infinite in the proof for it to have been a proof at all.

[mnarayan01]

If you sufficiently specify the runtime environment the proof can still work: Since the array is composed of integers, many C compilers/machine architectures will dictate a maximum size of the array s.t. there can't be overflow.

[haimez]

Touche, and fair enough- although you would expect them to call out that limitation since it's both critical and highly un-general. Bytes are comparable, small, and common enough to at least accommodate an exclusionary statement in the proof.