strange behavior of by-value function arguments in postcondition

[bauss]

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