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


fckingspmfromu@gmail.com changed:

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


--- Comment #33 from fckingspmfromu@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: -------

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


timon.gehr@gmx.ch changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |chalucha@gmail.com

Bug 6856 depends on bug 11835, which changed state.

Bug 11835 Summary: Assert not thrown from contract https://d.puremagic.com/issues/show_bug.cgi?id=11835

           What    |Old Value                   |New Value
----------------------------------------------------------------------------
             Status|NEW                         |RESOLVED
         Resolution|                            |DUPLICATE

--- Comment #34 from timon.gehr@gmx.ch 2013-12-29 16:40:55 PST ---
*** Issue 11835 has been marked as a duplicate of this issue. ***

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