strange behavior of by-value function arguments in postcondition

[FeepingCreature]

On Friday, 3 September 2021 at 06:53:40 UTC, bauss wrote:
> On Friday, 3 September 2021 at 06:50:35 UTC, FeepingCreature
>> But also, the `if (x < 10)` (really, `x <= 10`) test here is 
>> *why* you'd be justified in writing `in (i > 10)` later.
>
> You haven't told the compiler that x will always be > 10. You 
> have told the compiler that you expect it to always be above 10 
> but it might not be, say if the value came from user-input or a 
> file somewhere in the call-chain. You have no way to guarantee 
> that something always is something for the compiler, UNLESS the 
> value can never come from a dynamic source.

You have a way to guarantee that something always is something - 
and you've already shown how: `if (i <= 10)`. The `if` justifies 
the `in`.

If I expect `i` to be above 10 but it might not be, I write `if` 
and return an error. If I expect `i` to always be above 10, but 
want to sanity check or codify the assumption, I write `assert`.

I think when you write `assert(i > 10)` in any form, then `i` 
being `<= 10` past that point should be illegal, ie. value range 
propagation should be able to rely on asserts having excluded 
parts of the range.