strange behavior of by-value function arguments in postcondition

[Andrzej K.]

On Tuesday, 31 August 2021 at 11:40:42 UTC, Mike Parker wrote:
> On Tuesday, 31 August 2021 at 10:43:41 UTC, Andrzej K. wrote:
>
>> I would intuitively assume that the contract of such a 
>> function is: "I will not modify your objects, and I will 
>> select a number from the range that your objects indicate."
>
> For the first half of that assumption to be valid, you would 
> need this function signature:
>
> ```d
> int select(const int lo, const int hi) {}
> ```

I partially agree with this. I agree with the part that if I 
declare the by-value arguments as `const` then I can safely refer 
to their names in postconditions. (I use my definition of 
"safely", as explained in the beginning of this thread.)

However, taking arguments by value (`const` or not) *always* 
means that I do not modify the caller's objects. This is part of 
the deal: I make a copy in order not to modify the original. I do 
not have to declare by-value arguments `const` in order to 
guarantee that I do not modify the original objects used by the 
caller to invoke my function.

I guess, the question here is, who are the postconditions for? 
Are they for the caller (to guarantee something that the caller 
understands)? Or are they for the callee (in order to 
automatically inject assertions into function body)? If it is the 
latter, then the current semantics are fine.