strange behavior of by-value function arguments in postcondition

FeepingCreature feepingcreature at gmail.com
Fri Sep 3 05:47:32 UTC 2021


On Friday, 3 September 2021 at 00:23:48 UTC, deadalnix wrote:
> More specifically, the in condition is a contract that concern 
> the caller - in some way the user of the code. You'll not that, 
> because the in condition is a failure of the caller, then what 
> DMD does is wrong - the contract needs to be at the call site. 
> You might that this is just an implementation detail, but it is 
> in fact very relevant for contract on polymorphic functions, 
> which will do the wrong thing with the current implementation.
>

You have a point, but it's debatable.

To elaborate, let's consider:

```
class A { void foo(int i) in (i > 10) { } }
class B : A { override void foo(int i) in (i > 0) { } }

void main() {
   A a = new B;
   a.foo(5);
}
```

What do we know about `a.foo`? We know it's a method of `A`, 
which has an incondition of `i > 10`. So `a.foo(5)` *should* by 
all rights error out. It doesn't, because through the grace of 
our `new B` we have an object that has *actually* relaxed the 
contract.

This actually relates to the matter of common vs civil law, and 
what in the beautiful German language is called the "umgekehrte 
Tatbestandsirrtum", or "inverted offense presence misconception". 
(Isn't German beautiful?) To my knowledge, the US doesn't have 
the same concept, but it's effectively an inverted mistake of law.

Essentially, because civil law lawyers are nerds, they apply the 
following logic:

- if one (reasonably) *doesn't* know one is committing a crime, 
one cannot be guilty
- so if you *think* you are committing a crime while what you're 
doing is actually legal, your action is punishable, because 
symmetry is beautiful or something.

(Disclaimer: not a lawyer.)

The same thing applies here. It is legal to call `a.foo(5)` 
because `a` is secretly a `B` object. But since you don't know 
this, you are committing a reverse mistake of law: thinking 
something is illegal, when it actually isn't, and doing it 
anyway. So in a common law language like D this passes, but in a 
civil law language, ie. with asserts at the callsite, it would 
error.


More information about the Digitalmars-d mailing list