Though Shaw raises a valid point based on the fact that we program in more diverse and hostile situations today than K&R did back in their days, I'm unsure how deep one needs to go into program correctness when teaching a language. Wouldn't it suffice, for example, to have program correctness highlighted as a chapter?
Take this -
> Also assume that the safercopy() function uses a for-loop that does not test for a '\0' only, but instead uses the given lengths to determine the amount to copy.
It is possible to write a safercopy() conforming to that loose specification that will not terminate. Just make the test something like "i != length" instead of "i < length". Then you can supply negative length arguments and get it to fail. Of course, that would be stupid, but it already illustrates the art of specification. .... Well, with finite precision integers, "i != length" would terminate at some point due to wrap around, but would take the universe to end if you'd used 128bit integers. To do it even more simply, `safercopy(1,2,3,4)` can crash the program.
Is the moral of this story that programs are not valid outside the context they were created for? .. or is it to never use data structures whose integrity cannot be proved without failure? .. or is it that proving a program's correctness using some method only indicates a failure of imagination? .. or, to put it differently, that you can only prove a program wrong but never one right?
Take this -
> Also assume that the safercopy() function uses a for-loop that does not test for a '\0' only, but instead uses the given lengths to determine the amount to copy.
It is possible to write a safercopy() conforming to that loose specification that will not terminate. Just make the test something like "i != length" instead of "i < length". Then you can supply negative length arguments and get it to fail. Of course, that would be stupid, but it already illustrates the art of specification. .... Well, with finite precision integers, "i != length" would terminate at some point due to wrap around, but would take the universe to end if you'd used 128bit integers. To do it even more simply, `safercopy(1,2,3,4)` can crash the program.
Is the moral of this story that programs are not valid outside the context they were created for? .. or is it to never use data structures whose integrity cannot be proved without failure? .. or is it that proving a program's correctness using some method only indicates a failure of imagination? .. or, to put it differently, that you can only prove a program wrong but never one right?