strange behavior of by-value function arguments in postcondition

[bauss]

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;
}
```