You're Doing In-Conditions Wrong

burt invalid_email_address at cab.abc
Tue Jul 14 10:19:51 UTC 2020


On Monday, 13 July 2020 at 13:55:56 UTC, FeepingCreature wrote:
> [...]
>
> Let's consider two cases: debug modes, where we want to look 
> for and find logic errors, and non-debug mode, where we just 
> want to run correctly.
>
> Within debug mode, D should enforce that in contracts loosen 
> the conditions. As such, it should always execute both 
> superclass and subclass contract and Error if superclass-in 
> passes but subclass-in does not.

I don't believe this is actually the case; it should not throw an 
Error if superclass-in passes and subclass-in does not. Consider 
the following case:

```
class A {
     /// Postconditions: `x` must equal `2`.
     void method(int x) in (x == 2) {}
}
class B : A {
     void method(int x) in (x == 3) {}
}

auto b = new B;
b.method(3); // valid
b.method(2); // valid, since `B` is-an `A` and `A.method` 
guarantees that inputs that pass x == 2 are valid.

A a = b;
a.method(2); // valid, even though this passes superclass-in but 
not subclass-in
a.method(3); // dangerous! `A.method` does not guarantee that x = 
3 is allowed!
```

This is perfectly valid code, since the signature of `A.method` 
guarantees that it may take any inputs that are `x == 2`. The 
relationship is "super-in || sub-in" (an OR-relationship). [0]

> In other words:
>
> try {
>   superMethod.runInCondition();
> } catch (Exception) {
>   // if this throws, all is well - the input is just not 
> accepted.
>   method.runInCondition();
>   // if it didn't throw, all is well - the overridden in 
> contract loosened the condition
>   return;
> }
> // super method accepted this input - confirm that our logic 
> holds
> try {
>   method.runInCondition();
> } catch (Exception) {
>   throw new LogicError("in contract was tightened in subclass - 
> this is illegitimate");
> }
> But what to do outside debug mode? In my opinion, the 
> reasonable thing to do is to only run the child contract.

This is not possible: input that passes the `in`-contract of the 
superclass should also be guaranteed to be valid input, if the 
child contract does not pass. After all, inputs that are valid 
for the superclass's implementation should also be valid for the 
subclass's implementation.

> Why? Well, consider the case that the parent contract is more 
> tight than the child contract. In that case, the parent may 
> throw an informative exception, but we don't care because we 
> ignore it anyway; here, the parent's contract provides no 
> information.
>
> However, consider the case that the parent contract is more 
> loose than the child contract. In that case, the child contract 
> has *more* information than the parent. In the debug case, we 
> want a LogicError in this scenario. However, the second-best 
> thing is the exception that the child provides. Again, the 
> parent contract has nothing to add, and we should just run the 
> child contract.
>
> Further benefits: this will also fix weirdnesses such as
>
> interface I { void foo(); }
> class C : I { void foo() in(this.is.never.compiled) { } }

This is valid, but should probably emit an error, since `I.foo` 
has no in-contracts and will always pass, so `C.foo`'s condition 
will never have to be checked (like you said).

> interface I { void foo() in(true); }
> class C : I { void foo() in(false) { } }
> which would then be a compiletime error or runtime error, 
> respectively.

This is exactly the same case as above: `I.foo` will always pass 
and as a result, `C.foo` does not have to be checked.

> Programming languages should do reasonable things. No 
> reasonable programming language, when faced with this code,
>
> void foo(int i)
> in (i > 5)
> {
>   assert(i > 5, "this cannot happen");
> }
>
> should ever fail with "this cannot happen".

In fact, when in-contracts are disabled, `foo(5)` may decide to 
fail with "this cannot happen", crash, corrupt memory or fail 
with "ERROR", since continuing execution while the in-contract 
has failed is UB anyway!

-burt

[0] https://dlang.org/spec/contracts.html#in_out_inheritance



More information about the Digitalmars-d mailing list