3 ms·
It is simple, short and obviously correct. You don't have to record every single line of reasoning in a proof or argument, when the intermediate steps are obvio
by milesrout 2y ago
It is simple, short and obviously correct. You don't have to record every single line of reasoning in a proof or argument, when the intermediate steps are obvious. Same applies here. It isn't necessary to document this because it is obvious from a glance that it is correct. You can derive its correctness with a moment's thought. So it is fine not to assert it - that would be clutter.
- Joker_vD 2y ago> obviously correct While it is "obvious" that it is correct, it is, in fact, neither obvious nor correct if A. you ever subtract from then len field, and B. you use "len != 0" as a check for "is string non-empty". This program does both things quite a lot and it requires a conscious check to re-assure yourself that no, in this particular program, the patterns of acitons A (subtractions from the len field) never break the property B (non-zero len means that the string is not empty). But any minor modification may accidentally break this harmony if you are not aware that it is required to hold.