3 ms·
> the algorithm will wrongfully report "false" for arrays like e.g. [INT_MIN, -1] `INT_MIN + -1` is not 0 so it should report false in that case. For UINT_MAX
by Jtsummers 1y ago
> the algorithm will wrongfully report "false" for arrays like e.g. [INT_MIN, -1]
`INT_MIN + -1` is not 0 so it should report false in that case.
For UINT_MAX, the algorithm would need to be reconsidered, though, since it's written with signed integers in mind.
> Hopefully the proof would break if one tried to transfer it over?
Hopefully. The proof would have to be modified to account for the actual types. If you're using bounded integers you'd need to write a different proof.
- derdi 1y ago> For UINT_MAX, the algorithm would need to be reconsidered, though, since it's written with signed integers in mind. The algorithm is written assuming that unary - produces the additive inverse. That is also true for C's unsigned integers. -1U == UINT_MAX, -UINT_MAX == 1U. It Just Works.
- junon 1y agoINT_MIN - 1 is undefined behavior in C.
- deleted 1y ago[deleted]