Shortcut evaluation for hierarchy of in contracts

[Timon Gehr]

Daniel Murphy wrote:
> "Walter Bright" <newshound2 at digitalmars.com> wrote in message
> news:iuju03$27ip$1 at digitalmars.com...
>> The 'in' contract must pass at least one of the 'in' contracts of its
>> inheritance hierarchy.
>> Derived functions "loosen" the requirements for input.
>
> This might be the recommended way to do it, but this is not enforced by the
> compiler, just assumed.
>
> To enforce this, the compiler should give an error if a base function's
> precondition passes but a derived precondition does not.
>
> The requirement is not really that any 'in' contract passing is good enough,
> it's just assumed that all preconditions on inherited functions will pass if
> the base contract does.

Actually that is not true. One passing contract is enough. The current (and
correct) behavior enforces that when the parents contract passes, the child's
contract passes too.

If both had to pass, a child class could actually make contracts more restrictive.
It is this what we want to avoid, right?

The mistake is to assume, that the in contract of the child classes method
consists of what is written there only.
But arguably that is a problem with the language. Compare CP in D to Bertrand
Meyer's DBC in Eiffel:

//D
class Foo{
  void bar(int a, int)
  in{assert(a>0);} // require that a>0
  out(r){assert r>0;}
  body{
    return a;
  }
}

class Qux : Foo{
  override void bar(int a,int b)loosen
  in{assert(b>0);} //'if parents contract fails, I can still produce sensible
behavior if b>0 holds'
  body{
    return a>0?a:b;
  }
}

--Eiffel
class Foo
feature
  bar(a,b:INTEGER)
    require
      a_positive: a>0
    do
      Result:=a
    ensure
      result_positive: Result>0
    end
end

class Qux
inherit
  Foo
    redefine bar end
feature
  bar(a,b:INTEGER)
    require else    -- important!
      b_positive: b>0
    do
      if a>0 then Result:=a
      else Result:=b
    end
end

As you can see, in Eiffel, contract extension has a different syntax than contract
definition. ('require else' vs. require) In D the syntax is identical, even though
the two things done are quite different. What effectively is done depends on
whether or not the override keyword is present. I assume it is this that has led
to the misunderstanding.

Now, sure, if the parents contract is

in{assert(a<=10);}

and the child's contract is

in{assert(a<=5);}

then that is almost certainly an error because the child's contract fails to
loosen any restrictions.
But to catch this in the general case, the compiler would have to incorporate a
theorem prover.
(And validity of D code would start to depend on the quality of the theorem prover
of the respective D compiler ;))

Cheers,
-Timon