[Issue 16975] New: Top-level assert in contracts must be distinct from general assert

[via Digitalmars-d-bugs]

https://issues.dlang.org/show_bug.cgi?id=16975

          Issue ID: 16975
           Summary: Top-level assert in contracts must be distinct from
                    general assert
           Product: D
           Version: D2
          Hardware: All
                OS: All
            Status: NEW
          Severity: enhancement
          Priority: P1
         Component: dmd
          Assignee: nobody at puremagic.com
          Reporter: andrei at erdani.com

This is mostly an implementation matter, but it should help us (a) make the
working of contracts more rigorous, and (b) make contracts faster.

Consider:

void fun(R)(R r) if (isInputRange!R && is(ElementType!R == int))
in { assert(r.front == 42); }
body { ... }

This code has a contract stating that the front element of the range is equal
to 42. There is also an implied assumption that the range is not empty. The
range may, however, be empty and may signal that by throwing an AssertError, a
RangeError, some Exception object, etc. It is generally not specified how a
range shall enforce its own preconditions. Consequently, this onus cannot fall
on the shoulders of the contract of fun().

Generally there is a distinction between the assertions stated at top level
inside a contract, and whatever other assertions do. Generally a failing assert
is considered an unrecoverable error; however, in contracts that cannot be the
case. It follows that precondition-level asserts are qualitatively distinct
from asserts in arbitrary code.

In the particular example above, the formulation may be arguably a bug in the
formulation of the contract itself. If it is part of the precondition that the
range is not empty, that should be assert(!r.empty && r.front == 42).

There is precedent with failing asserts being handled differently: in
unittests, a failing assert invokes a different function than a failing assert
elsewhere.

Top-level asserts in preconditions should be lowered to simple code that checks
a Boolean and set a flag to (or return internally) false if the assertion
fails. Then the flag can be combined with that of inherited/derived conditions
etc.

--