strange behavior of by-value function arguments in postcondition

[Andrzej K.]

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?