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:

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:

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?

On Tuesday, 31 August 2021 at 10:43:41 UTC, Andrzej K. wrote:

int select(int lo, int hi)
  in (lo <= hi)
  out (r; lo <= r && r <= hi)
{
  int ans = lo;
  lo = hi; // why not
  return ans;
}

void main()
{
    int lo = 1;
    int hi = 4;
    int i = select(lo, hi);
    assert(lo == 1);
    assert(hi == 4);
    assert(i >= 1 && i <= 4);
}

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

On Tuesday, 31 August 2021 at 11:30:16 UTC, bauss wrote:

int select(int lo, int hi)
  in (lo <= hi)
  out (r; lo <= r && r <= hi)
{
  int ans = lo;
  lo = hi; // why not
  return ans;
}

void main()
{
    int lo = 1;
    int hi = 4;
    int i = select(lo, hi);
    assert(lo == 1);
    assert(hi == 4);
    assert(i >= 1 && i <= 4);
}

Yep, I was right.

Looking at the AST this is what the compiler generates for the function:

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

On Tuesday, 31 August 2021 at 10:43:41 UTC, Andrzej K. wrote:

For the first half of that assumption to be valid, you would need this function signature:

int select(const int lo, const int hi) {}

On Tuesday, 31 August 2021 at 11:40:42 UTC, Mike Parker wrote:

int select(const int lo, const int hi) {}

And holds true because this statement is then disallowed:

  lo = hi; // why not

Which means "lo" can never be modified or rather never will be modified. At least in this context considering it's a value-type. If it was a reference type then obviously it could still change as external sources can modify it and only immutable would guarantee that it stays the same.

On Tuesday, 31 August 2021 at 11:40:42 UTC, Mike Parker wrote:

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.

On Tuesday, 31 August 2021 at 12:35:54 UTC, Andrzej K. wrote:

The postconditions are for the maintainer to ensure the function actually works as expected.

If the asserts don't pass then the function has a bug.

Assert statements are never for the user and always for the maintainer.

On Tuesday, 31 August 2021 at 11:33:10 UTC, bauss wrote:

int select(int lo, int hi)
  in (lo <= hi)
  out (r; lo <= r && r <= hi)
{
  int ans = lo;
  lo = hi; // why not
  return ans;
}

void main()
{
    int lo = 1;
    int hi = 4;
    int i = select(lo, hi);
    assert(lo == 1);
    assert(hi == 4);
    assert(i >= 1 && i <= 4);
}

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.

On Tuesday, 31 August 2021 at 12:39:59 UTC, bauss wrote:

Yup. This explanation is compatible with what the compiler does.

What puzzles me now is that if it is for implementer only, why should it be the part of the function signature (as opposed to the function body).

On Tuesday, 31 August 2021 at 12:45:29 UTC, Andrzej K. wrote:

I think it's just because it's better to separate asserts from functionality. It makes it much more readable, especially for larger functions etc.

It also makes it possible to assert the return value from functions with multiple return statements but in a single place.

Otherwise you'd have to do something hacky or use scope statements, which ultimately ends up being extra boilerplate.