3 ms·
> Satisfying preconditions is a requirement to make functioning programs. > The insanity would be assuming that every function is valid for the Cartesian produ
by Joker_vD 2y ago
> Satisfying preconditions is a requirement to make functioning programs.
> The insanity would be assuming that every function is valid for the Cartesian product of all possible of its arguments.
Would it? That reminds me of a recent post on HN about proving the long (binary) division algorithm with Hoare's logic. It uses the "d > 0" precondition and proves that, indeed, the algorithm arrives at the required postcondition. However, the algorithm still terminates and produces something even when d == 0. What does it computes in this case? Is it useful? Should such questions even be considered?
- grandempire 2y ago> Should such questions even be considered? Yes, a better understanding of the problem gives you a better understanding of the preconditions. Always ask if you have that right and weaken accordingly.