[Issue 6857] Precondition contract checks should be statically bound.

[Max Samukha]

On Saturday, 5 May 2012 at 05:57:31 UTC, Don wrote:
> http://d.puremagic.com/issues/show_bug.cgi?id=6857
>
>
>
> --- Comment #46 from Don <clugdbug at yahoo.com.au> 2012-05-04 
> 22:58:38 PDT ---
> (In reply to comment #45)
>> (In reply to comment #44)
>> > But going by comment 26, there is no breakage of correct OOP 
>> > behaviour
>> > involved.  So how is this relevant?
>> 
>> This has already been covered. We're going in circles.
>
> Walter, you haven't understood this at all. None of us have 
> claimed that the
> program ever gets into a wrong state.
> Let me try another way.
> Given a module which consists of:
> ----------
> struct F {
>    void foo(int n) in { assert( n > 0); } body {}
> }
>
> void xyzzy(F f)
> {
>     f.foo(-1);
> }
> ----------
> A theorem prover, or even a compiler that did basic range 
> checking for
> preconditions, should raise an error at compile time. Not at 
> run time when it's
> actually called with an F, but at compile time. Nothing 
> controversial there.
>
> Now, change F from a struct to a class. We believe that the 
> code should still
> fail to compile.

Why would one expect the same behavior after changing the struct 
to a class? The call to foo in the case of struct is statically 
bound. f.foo *cannot* be bound to any other function than the one 
declared in F, so it is *always* safe for compiler/theorem prover 
to statically check the precondition.

Classes are a different story because of dynamic binding. There 
will be cases where compiler/theorem prover will be able to 
determine the static type at compile time and detect the error 
early. Otherwise, it is obvious that the precondition must be 
checked on the dynamic type at run-time.