On Saturday, 5 May 2012 at 05:57:31 UTC, Don wrote:

--- Comment #46 from Don <clugd...@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)
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.

Reply via email to