strange behavior of by-value function arguments in postcondition

[Andrzej K.]

On Tuesday, 31 August 2021 at 11:33:10 UTC, bauss wrote:
> On Tuesday, 31 August 2021 at 11:30:16 UTC, bauss wrote:
>> On Tuesday, 31 August 2021 at 10:43:41 UTC, Andrzej K. wrote:
>>> Have a look at the following short example:
>>>
>>> https://d.godbolt.org/z/1KoofEx5Y
>>>
>>>
>>> We have a function that takes arguments by value and has a 
>>> postcondition that refers to these arguments:
>>>
>>> ```D
>>> int select(int lo, int hi)
>>>   in (lo <= hi)
>>>   out (r; lo <= r && r <= hi)
>>> {
>>>   int ans = lo;
>>>   lo = hi; // why not
>>>   return ans;
>>> }
>>> ```
>>>
>>> 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." 
>>> This expectation of mine can be reflected by the following 
>>> assertions:
>>>
>>> ```D
>>> void main()
>>> {
>>>     int lo = 1;
>>>     int hi = 4;
>>>     int i = select(lo, hi);
>>>     assert(lo == 1);
>>>     assert(hi == 4);
>>>     assert(i >= 1 && i <= 4);
>>> }
>>> ```
>>>
>>> The fact that function `select()` modifies its copy of the 
>>> argument, should not be of interest to the caller: it is an 
>>> implementation detail of the function. And all the assertions 
>>> in function `main()` are satisfied. However, the fact that 
>>> postcondition observes the copies of user objects makes the 
>>> postcondition fail.
>>>
>>> I realize that this effect is consistent with the mechanics 
>>> of the language. But it seems that the mechanics of the 
>>> language render the postconditions somewhat counterintuitive. 
>>> The postcondition should reflect the contract: it should 
>>> describe something that the caller can also see and 
>>> understand: not the state of internal copies of user input.
>>>
>>> Is this not a design bug?
>>
>> To me it makes perfect sense as the function would probably 
>> translated to something like this:
>>
>> int select(int lo, int hi)
>> {
>>   // in
>>   assert(lo <= hi);
>>
>>   // body
>>   int ans = lo;
>>   lo = hi;
>>
>>   // out
>>   int r = ans;
>>   assert(lo <= r && r <= hi);
>>
>>   return r;
>> }
>
> Yep, I was right.
>
> Looking at the AST this is what the compiler generates for the 
> function:
>
> ```d
> int select(int lo, int hi)
> in (lo <= hi)
> out (r; lo <= r && (r <= hi))
> {
> 	{
> 		assert(lo <= hi);
> 	}
> 	int ans = lo;
> 	lo = hi;
> 	__result = ans;
> 	goto __returnLabel;
> 	__returnLabel:
> 	{
> 		const ref const(int) r = __result;
> 		assert(lo <= r && (r <= hi));
> 	}
> 	return __result;
> }
> ```

Thanks. This seems to imply that postconditions are a way to 
automatically inject assertions into function body. And then the 
postconditions behave as one would expect.

However, my understanding of postconditions is that they 
constitute a part of the function's interface that means 
something to the caller, even in the absence of the function 
body. The caller can never be interested if the function's 
current implementation mutates its copies of the arguments or 
not. And the contract of the function cannot change only because 
we have mutated the copies of function arguments.