Daniel Murphy wrote:"Timon Gehr" <timon.g...@gmx.ch> wrote in message >news:iukptu$10nq$1...@digitalmars.com... >> Daniel Murphy wrote: >>> "Timon Gehr" <timon.g...@gmx.ch> wrote in message >>> news:iukoge$u82$1...@digitalmars.com... >>>> How would you catch it? I am sure it cannot be caught trivially: >>>> >>>> There are 4 possibilities: >>>> 1. Both parent and child contract would pass. >>>> 2. Parent passes, child would fail. >>>> 3. Parent fails, child passes. >>>> 4. Parent fails, child fails. >>>> >>> In case 2, the contract is invalid. >>> >>> In reality, the overriding graph forms a tree, and the contract is >>> invalid >>> if any precondition passes if its parent's precondition fails. (the root >>> being the most derived function) >> >> That is case 3. And it is perfectly valid. >> > > Sorry for the mixin of terms, I meant parent in the tree, which is the > opposite direction to parent in inheritance. > >>> >>> It is definately possible to implement runtime checking to enforce this. >> >> My first post on the subject features an example where case 2 can occur >> and be >> valid. Have a look at it please. >> > > I disagree. If the child's in condition requires something that the > parent's didn't, you've just tightened the precondition. > > If I understand correctly, it's equivilent to: > parent: require a is greater than 0 > child: require b is greater than 0
It is equivalent to: parent: require a is greater than 0 child: ... else require b is greater than 0 > > In this case, the parent allows more values of b than the child does, so the > precondition has been tightened. No, the child allows arbitrary values of b if a>0, due to the short-circuiting behavior. > [snip.] >> >> Again: in contract of child != precondition of child >> > > Ok, I doubt I used the right terms everywhere. I didn't either :). > Reading your other post, I'm starting to think we just have different ideas > of how contract inheritance should work. I _think_ mine is in line with how > it is supposed to work in D. I think mine is in line with how it is supposed to work, based on the following facts: 1. It is how it currently is implemented. 2. It is how it works in Eiffel. The site on Contract Programming has a reference to DBC in Eiffel. 3. Yours requires that all child classes duplicate the precondition of their parents in their in-contracts. (which will then be ensured by a runtime check.). > If you could post some D examples that would help, doing this all in my head > is starting to hurt. Sure, if you remember the Foo/Qux example (Foo is parent, Qux is child, method bar(a,b), parent requires a>0 child requires else b>0) void main(){ auto a=new Foo, b=new Qux; a.bar(1,-1);//ok b.bar(1,-1);//ok, child works everywhere parent works //a.bar(-1,1);// not ok //b.bar(-1,-1)// not ok b.bar(-1,1);//ok, child works too if b>0 } > > I'm fairly confident a runtime test can catch the following case: Yes but that is not correct in general (unless the behavior is changed to reflect your ideas). The two contracts could be uncorrelated. [snip] Cheers, -Timon