Maybe D was wrong on contracts

[Quirin Schroll]

TL;DR: D’s contracts are theoretically unsound, but there’s an 
easy fix.

---

I just read 
[P3097](https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2026/p3097r3.pdf), an accepted proposal for C++29. It allows for pre- and postconditions on virtual member functions. Its design goals and discussion sections (§§ 3–4) are really interesting as they discuss (among others) the design of D’s contracts. (You don’t need to know any C++ to follow most of the proposal sections.)

Here’s the, in my opinion, most crucial paragraph for the D 
community. “It” refers to the design of prior proposals that were 
similar to D’s and Eiffel’s contracts, which closely follow the 
Liskov substitution principle:
> [It] assumes that contract assertions can express the entire 
> plain-language contract across the whole program, while in 
> reality they will only ever express a subset of it, and only in 
> some components. Our proposed C++ design accounts for this 
> fundamental limitation, ensures that introducing contract 
> assertions cannot cause remote breakage of correct code, and 
> enables the user to adopt precondition and postcondition 
> assertions on virtual functions incrementally.
>
> […]
>
> More fundamentally, OR-ing two sequences of *contract 
> assertions* is not equivalent to OR-ing the two contracts that 
> those assertions check. As we saw above, contract assertions 
> can only validate a subset of a function’s plain-language 
> contract. Therefore, assuming that one side of such a 
> disjunction is satisfied merely because none of the associated 
> assertions failed is logically unsound.

In § 4.7, P3097 exemplifies how the mantra of OR-ing and AND-ing 
is incorrect (overly narrow) if the goal is to enforce the 
substitution principle. I won’t bore you with the example; in 
short: If a virtual function has a precondition *P* and 
postcondition *C* (read *C* as conclusion), any implementation 
must satisfy the implication *P* ⇒ *C.* Thus, for the 
substitution principle to hold, any overriding function must also 
satisfy *P* ⇒ *C,* but the current state of the D language 
requires it to actually satisfy *P* ∨ *Q* ⇒ *C,* where *Q* is the 
conjunction of the preconditions of the overrider. Notably, *Q* 
might be `true` when the preconditions of the overrider are the 
empty set.

Maybe C++ got something right, or rather, D got something wrong 
that C++ got right-er:

*A virtual function’s postconditions don’t get limit what 
overriders do when invoked with arguments that don’t satisfy its 
preconditions.*

The violation of this principle might be the reason why D’s 
contracts never took off.

It might be worth considering moving closer to C++’s semantics of 
contracts, not because of interoperability or compatibility, but 
because they’re closer to correct.

D should validate contracts differently and in-line with the 
following principle:

*The postconditions of a function need only be met by its 
implementation if its precondition was satisfied.*

For non-virtual functions, the violation of preconditions simply 
leads to an `Error` being thrown, thus skipping the code that 
checks the postconditions, thus coincidentally satisfying the 
principle. It fails only for virtual functions.

Example:
```d
class Base           {          int f(int x) in(x > 0) out(r; r > 
0); }
class Derived : Base { override int f(int x) in(true)  out(r; 
true ); }
```
If we assume both implementations are just `{ return x; }`, all 
contracts should be satisfied because with `r == x`, all 
individual contracts are of the form *X* implies *X,* which is 
obviously true.

Where D is going astray is not that when calling `Derived.f`, it 
checks if `Base.f.in` is satisfied at all, but what it does with 
the result. Current behavior is: `Derived.f` cannot assume 
anything (because `Derived.f.in` is `true`) and must definitively 
establish `r > 0` because `Base.f.out` says so and in the current 
language semantics, all postconditions have to be met 
unconditionally. This is logically incorrect because `Base.f.out` 
need only be satisfied if `Base.f.in` was satisfied to begin with 
(that’s what a contract actually means); if it wasn’t satisfied, 
`Derived.f` should not be bound by `Base.f.out` in any way.

I have no idea how DMD implements contract checking, but I assume 
it wouldn’t be too difficult to skip checking postconditions if 
the corresponding preconditions hadn’t been met. At worst, it has 
to store a `bool` to remember that. I’d consider this a miniscule 
price to pay (in terms of performance) for a contract semantics 
that is theoretically sound.

C++29, according to the proposal, given an object with a static 
type of `C`, the language wouldn’t consider the contracts of 
`Base.f` at all. The reasoning is: If we *know for sure* we have 
a `C` object, only contracts specified on `C` concern us, as well 
as contracts of the dynamically invoked function; this 
(intentionally) allows for violations of the substitution 
principle for cases where no plain substitution takes place. I’m 
not proposing that at all, or rather, if anything, for 
`extern(C++)` functions only.