[Issue 6856] Absence of in contract (precondition) on override of method that has one is badly designed

[d-bugmail at puremagic.com]

https://d.puremagic.com/issues/show_bug.cgi?id=6856


fckingspmfromu at gmail.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |fckingspmfromu at gmail.com


--- Comment #33 from fckingspmfromu at gmail.com 2013-11-30 02:42:07 PST ---
A weaker precondition B compared to the stronger precondition A is in the
mathematical and logical sense an implication:

A -> B

That means firstly, whenever the precondition A is met then the weaker
condition
B _must_ be met, too. Also logically this means:

not B -> not A.

As B has the weaker condition, every time B is not met, A _must_ not be met
too. This is because B meets _at least_ all cases that A meets. This is the
definition of a weaker condition.

Also: 
    interface A {
        void foo() 
        in { 
            // strong precondition 
        }
    }

    class B : A {
        override void foo() 
        in { 
            // weaker precondition 
          } 
        body {
        }
    }

    A a = new B();
    a.foo(); // The precondition of A must be checked.

    B b = new B();
    b.foo(); // The precondition of B must be checked.


Also in the above example's call a.foo(), we must use the static type A to
determine the precondition. If we would take the precondition of type B in
consideration, we would check a too weak precondition. this violates the Liskov
substitution principle! 
In the call b.foo() we must only check the precondition of type B as this is
the weaker one. If it succeeds all is fine. If it fails then the precondition
of A would fail too, as B covers at least all cases in which of A does not fail
(see the implications at the top).

Also I recommend to force every derived precondition to enforce the use of a
keyword like "weaken" to explicitly show that this must be a weaker
precondition:

    class B : A {
        override void foo() 
        weaken in { 
            // weaker precondition 
          } 
        body {
        }
    }

-- 
Configure issuemail: https://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------