[Issue 6857] Precondition contract checks should be statically bound.
https://issues.dlang.org/show_bug.cgi?id=6857 --- Comment #89 from Andrei Alexandrescu --- To clarify: this issue is preapproved and is waiting for an implementation. --
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 jens.k.muel...@gmx.de changed: What|Removed |Added CC||jens.k.muel...@gmx.de --- Comment #1 from jens.k.muel...@gmx.de 2012-03-01 07:22:17 PST --- Can you elaborate why the static type must be considered? What's the problem with using the dynamic type? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
deadalnix changed:
What|Removed |Added
CC||deadal...@gmail.com
--- Comment #2 from deadalnix 2012-03-01 07:40:10 PST ---
(In reply to comment #1)
> Can you elaborate why the static type must be considered? What's the problem
> with using the dynamic type?
The problem is simple. Let's consider a class A and a subclass B.
Then a function as this :
void fun(A a) {
a.foo();
}
If passed an element of type B, fun will work, because B is a subclass of A. If
B.foo's contract is different than A.foo's, then B.foo's in contract is
executed.
It is a bug, because fun has no knowledge weither it manipulate an element of
type A or an element of type B. It means that fun must respect the in contract
provided by A.foo, because in other case, it may or may no work, depending on
how fun in called, which isn't a reliable behavior.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #3 from jens.k.muel...@gmx.de 2012-03-02 00:35:52 PST ---
(In reply to comment #2)
> (In reply to comment #1)
> > Can you elaborate why the static type must be considered? What's the problem
> > with using the dynamic type?
>
> The problem is simple. Let's consider a class A and a subclass B.
>
> Then a function as this :
>
> void fun(A a) {
> a.foo();
> }
>
> If passed an element of type B, fun will work, because B is a subclass of A.
> If
> B.foo's contract is different than A.foo's, then B.foo's in contract is
> executed.
>
> It is a bug, because fun has no knowledge weither it manipulate an element of
> type A or an element of type B. It means that fun must respect the in contract
> provided by A.foo, because in other case, it may or may no work, depending on
> how fun in called, which isn't a reliable behavior.
Yesterday I was sleepy and wasn't able to understand it. But even now I fail to
see the issue.
First fun accepts any instance that is of class A or a subclass of A. And
independent of this whenever you call a.foo() all in contracts must be checked
using based on a's dynamic type.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
Don changed:
What|Removed |Added
CC||clugd...@yahoo.com.au
--- Comment #4 from Don 2012-03-02 01:57:16 PST ---
(In reply to comment #3)
> (In reply to comment #2)
> > (In reply to comment #1)
> > > Can you elaborate why the static type must be considered? What's the
> > > problem
> > > with using the dynamic type?
> >
> > The problem is simple. Let's consider a class A and a subclass B.
> >
> > Then a function as this :
> >
> > void fun(A a) {
> > a.foo();
> > }
> >
> > If passed an element of type B, fun will work, because B is a subclass of
> > A. If
> > B.foo's contract is different than A.foo's, then B.foo's in contract is
> > executed.
> >
> > It is a bug, because fun has no knowledge weither it manipulate an element
> > of
> > type A or an element of type B. It means that fun must respect the in
> > contract
> > provided by A.foo, because in other case, it may or may no work, depending
> > on
> > how fun in called, which isn't a reliable behavior.
>
> Yesterday I was sleepy and wasn't able to understand it. But even now I fail
> to
> see the issue.
> First fun accepts any instance that is of class A or a subclass of A. And
> independent of this whenever you call a.foo() all in contracts must be checked
> using based on a's dynamic type.
The point is that fun() must satisfy the precondition for A. The fact that it's
actually receiving a subclass of A is irrelevant.
Since subclasses of A can only widen the precondition, they don't need to be
checked. (Since they must pass A.in(), by definition they will pass A.in() ||
B.in()).
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 timon.g...@gmx.ch changed: What|Removed |Added Status|RESOLVED|REOPENED Resolution|INVALID | Severity|normal |enhancement --- Comment #6 from timon.g...@gmx.ch 2012-05-02 13:14:21 PDT --- (In reply to comment #5) > This report is invalid, I disagree. > it is working as designed. > Therefore the design is flawed and this report is an enhancement. > This is how inheritance of contracts and overriding of functions is supposed > to > work. > This report is not about how inheritance and overriding work, it is about static vs. dynamic binding. (Though inheritance and overriding of contracts also don't work how they are supposed to work, see issues 6856 and 7584.) > >void fun(A a) > >The point is that fun() must satisfy the precondition for A. > > This is incorrect. It must satisfy the precondition for A or any class derived > from A. How does it know which one to satisfy? If it does, it might as well just downcast the reference in order to get a wider interface. If it does not, it is a bug in fun() if it fails to satisfy the precondition for A. (It's signature claims it can handle all A's!) -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 Walter Bright changed: What|Removed |Added Status|REOPENED|RESOLVED Resolution||INVALID --- Comment #7 from Walter Bright 2012-05-02 14:11:46 PDT --- This is a misunderstanding about how inheritance works. If an A is passed to foo(), then only A's preconditions are checked. If a B is passed, then either A's precondition or B's precondition must be satisified. This is how standard inheritance works. I did not invent this. It is not a bug, and changing this behavior would completely break how inheritance works. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 timon.g...@gmx.ch changed: What|Removed |Added Resolution|INVALID |WONTFIX --- Comment #8 from timon.g...@gmx.ch 2012-05-02 15:10:01 PDT --- (In reply to comment #7) > This is a misunderstanding about how inheritance works. No, it is not. The precondition is what needs to be satisfied by the client of the method. The client has no way to know what exactly to satisfy if the precondition is dynamically bound, therefore the client usually has to assume that they have to satisfy the statically bound precondition. Failure to do so is a bug most of the time. I am not going to argue this further. It can probably go either way. The current behavior detects less bugs, but the proposed change would make writing contracts for certain cases cases where eg. a method accepts a parameter that has distinct restrictions depending on the result of a previous method invocation on the same object a little bit harder. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #10 from Walter Bright 2012-05-02 16:27:15 PDT --- I suggest checking Bertrand Meyer's book Object-Oriented Software Construction, which is the definitive reference on this. It's theoretically sound. I did not invent the design, I implemented it. The fundamental nature of 'in' contracts is that they are "loosened" on derivation. If an instance of B is passed to parameter A, then if either the contract for A or the contract for B passes, then it passes. It is NOT necessary for the A contract to pass. This is exactly what you're seeing in the example. If an instance of A is passed, then the contract for A must pass. It isn't a bug, it is the way it is supposed to work. Nor am I ignoring it - I'm trying to explain it. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 Andrei Alexandrescu changed: What|Removed |Added CC||and...@metalanguage.com Resolution|WONTFIX |INVALID --- Comment #11 from Andrei Alexandrescu 2012-05-02 16:40:01 PDT --- >The current specification is flawed. It have nothing to do with how >inheritance work (and I could assure you I know what I'm talking about, and >I'm also pretty sure Timon knows also). Mistakes happen to the best of us. In this case the specification is correct and the bug report is in error. Derived classes may require less and provide more, which in contract lingo translates into weaker "in" contracts and stronger�"out" contracts. This is not a matter in which reasonable people may disagree and not a matter of opinion. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #12 from deadalnix 2012-05-03 01:43:42 PDT ---
(In reply to comment #11)
> >The current specification is flawed. It have nothing to do with how
> >inheritance work (and I could assure you I know what I'm talking about, and
> >I'm also pretty sure Timon knows also).
>
> Mistakes happen to the best of us. In this case the specification is correct
> and the bug report is in error. Derived classes may require less and provide
> more, which in contract lingo translates into weaker "in" contracts and
> stronger�"out" contracts. This is not a matter in which reasonable people may
> disagree and not a matter of opinion.
I think you misunderstood what we are talking about here, as Walter is.
Nobody here discussed teh fact that in contract shouldn't become weaker when
inherited. This is, indeed, what corect OO design is.
What is discussed here is, with all details.
class A {
void foo() in { ... } body { ... }
}
class B : A {
override void foo() in { ... } body { ... }
}
then, let's consider :
fizbuzzA(A a) {
a.foo(); // A.foo's in contract is valid
}
fizzbuzzB(B b) {
b.foo(); // (A.foo OR B.foo)'s in contract is valid
}
The point is that B.foo's in contract loosen A.foo's in contract. And fizzbuzzA
have no knowledge of the fact that a subclass of A's instance can be passed.
So, if fizzbuzzA use foo with parameter that validate A.foo's in contract, but
not B.foo's in contract, it is an error. fizzbuzzA have no knowledge of the
runtime type of a, so shouldn't pass argument to foo that is invalid according
to A.foo's in contract. If it does, it means that fizzbuzzA is bugguy, or does
know about that fact that a isn't of type A, which is exactly what we DON'T
want when doing OOP.
It is Liskov substitution principle, any object of type B can be substituted to
an object of type A without the code using the object knowing about it. It is
probably the most important thing in OOP.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #13 from Andrei Alexandrescu 2012-05-03 07:05:18 PDT --- I apologize but I still think the confusion goes the other way. A good way to arbiter this is to peruse the literature on the subject, as Walter suggested. If going through a book has too much overhead, online articles and presentations should work, too. I can't afford to do much more explaining than essentially reciting material that's out there. For example I'd recommend this: http://www.cs.ucsb.edu/~bultan/courses/272-F08/lectures/Contract.ppt. Slides 19 and 20 should clarify the matter. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #14 from deadalnix 2012-05-03 10:45:19 PDT ---
(In reply to comment #13)
> I apologize but I still think the confusion goes the other way. A good way to
> arbiter this is to peruse the literature on the subject, as Walter suggested.
> If going through a book has too much overhead, online articles and
> presentations should work, too. I can't afford to do much more explaining than
> essentially reciting material that's out there. For example I'd recommend
> this:
> http://www.cs.ucsb.edu/~bultan/courses/272-F08/lectures/Contract.ppt. Slides
> 19
> and 20 should clarify the matter.
I did read your document with attention, and looked for some other resources
today. That arguments given in such documents validate both the current state
of thing and the proposed new behavior.
In fact, I have failed to find any documentation/article/whatever about the
corner case where both behavior differs.
In other terms, as it seems that the corner case hasn't been considered, the
proposed solution is *A* solution and not *THE* solution. As, according to
given arguments I have found in literature, both behavior are good.
If I restate arguments they goes like this :
- B can be written way after fizzbuzzA, so shouldn't be able to provide an in
contract that break it.
- Instance of B can be passed to any code that expect instance of A, so B in
contracts can only loosen contract provided by A, not restrict them.
I think we all agree on such points. I think we can all agree also that both
current behavior and proposed behavior satisfy constraints expressed here.
The only case where things differs is the one given as example above. Let's
remove the ... to make it fully explicit.
class A {
void foo(int x) in { assert(x > 0); } body {}
}
class B : A {
void foo(int x) in { assert(x > -2); } body {}
}
and the function
void fizzbuzz(A a) {
a.foo(-1);
}
If I do fizzbuzz(new B()); The current behavior will not raise any error. But,
as we see in fizzbuzz's body, it doesn't because the object is of type B, not
of type A, because any other instances of subtypes of A or A can cause the
fizzbuzz function to fail.
We conclude that the fizzbuzz function is only correct if it DOES KNOW that it
is manipulating object of type B, because operation done are invalid on object
of type A.
The erratic behavior of fizzbuzz will not be spotted if I pass an instance of B
to fizzbuzz. Still, the code is flawed and waiting to explode any time in the
future. The whole point of contract is to spot such a situation.
For valid code, both behavior allow the same thing exactly. The proposed
behavior allow to spot MORE problems EARLIER, and it is something you want.
The only reason fizzbuzz here is correct if because the programmer KNOW only
instances of B will be passed to fizzbuzz.
I may be wrong, but I'd be happy to discuss that specific case, instead of
relying on documentation that do not talk about it. I failed in finding
documentation about that specific corner case.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #15 from Walter Bright 2012-05-03
11:07:27 PDT ---
fizbuzzA(A a) {
a.foo(); // A.foo's in contract is valid
}
If an instance of B is passed to fizbuzzA, then the a.foo() will call B.foo(),
and either A.foo's in contract or B.foo's in contract must be valid.
There is no error or invalid corner case here.
I suspect that you think the contracts are checked based on static typing -
they are not, they are done using the virtual type.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #16 from Don 2012-05-03 11:56:47 PDT ---
(In reply to comment #15)
> fizbuzzA(A a) {
> a.foo(); // A.foo's in contract is valid
> }
>
> If an instance of B is passed to fizbuzzA, then the a.foo() will call B.foo(),
> and either A.foo's in contract or B.foo's in contract must be valid.
>
> There is no error or invalid corner case here.
>
> I suspect that you think the contracts are checked based on static typing -
> they are not, they are done using the virtual type.
This is the issue. WHY are they done based on the virtual type?
Checking the contracts based on static typing would detect logical errors in
the calling code. Doing it based on the virtual type ignores latent bugs in
specific instances where they are harmless. I can't understand why that's a
good idea.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #17 from deadalnix 2012-05-03 13:44:36 PDT ---
(In reply to comment #15)
> fizbuzzA(A a) {
> a.foo(); // A.foo's in contract is valid
> }
>
> If an instance of B is passed to fizbuzzA, then the a.foo() will call B.foo(),
> and either A.foo's in contract or B.foo's in contract must be valid.
>
> There is no error or invalid corner case here.
>
> I suspect that you think the contracts are checked based on static typing -
> they are not, they are done using the virtual type.
We are all well aware that the behavior you describe is the current behavior.
However we do think it is not optimal and can be improved because of the corner
case mentioned.
As you can see in given code, fizbuzzA is an invalid piece of code waiting to
explode in your face. And this is what you want to avoid, why we use so much
stuff like contracts and unit tests (and, as far as I am concerned in my
professional work, code review and static analysis tools).
The later the bug is discovered, the more expansive it is to fix, and, if it
goes in production, the more damage it can do. We want to avoid as much as we
can the risk of having a piece of code waiting to explode deep in the codebase.
fizzbuzzA is the typical example of the function that will cost you quite a
lot. It is flawed, and waiting to crash the application at any moment. We want
to detect that ASAP, and in contract should tell us that ASAP.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #18 from Walter Bright 2012-05-03 15:37:00 PDT --- (In reply to comment #17) > As you can see in given code, fizbuzzA is an invalid piece of code waiting to > explode in your face. There is no bug in example #14. Please show one where it blows up. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #19 from Walter Bright 2012-05-03 15:46:03 PDT --- (In reply to comment #16) > This is the issue. WHY are they done based on the virtual type? > Checking the contracts based on static typing would detect logical errors in > the calling code. Doing it based on the virtual type ignores latent bugs in > specific instances where they are harmless. I can't understand why that's a > good idea. The whole idea of polymorphism is to base things on the virtual type. I don't understand what latent bugs you are referring to. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 Stewart Gordon changed: What|Removed |Added CC||s...@iname.com --- Comment #20 from Stewart Gordon 2012-05-03 16:45:21 PDT --- (In reply to comment #5) > This is incorrect. It must satisfy the precondition for A or any > class derived from A. The in contract is part of the API of class A. If you call a method of A with arguments that don't satisfy this contract, you are not conforming to the API. (In reply to comment #10) > It isn't a bug, it is the way it is supposed to work. Nor am I > ignoring it - I'm trying to explain it. You're explaining the design you're copying. That's quite different from explaining why you've chosen to copy this particular design to the letter. (In reply to comment #19) > (In reply to comment #16) >> This is the issue. WHY are they done based on the virtual type? >> Checking the contracts based on static typing would detect logical >> errors in the calling code. Doing it based on the virtual type >> ignores latent bugs in specific instances where they are harmless. >> I can't understand why that's a good idea. > > The whole idea of polymorphism is to base things on the virtual > type. What are "things"? If you mean the effect of a call, then yes. This we seem to be all agreed on. If you mean whether a given call is legal, then you could by the same argument insist that called method names must be resolved in the context of the virtual type. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 Stewart Gordon changed: What|Removed |Added Status|RESOLVED|REOPENED Resolution|INVALID | --- Comment #21 from Stewart Gordon 2012-05-03 17:20:19 PDT --- Let's look at it another way. The relevant basic principle of inheritance is the ability to extend the functionality of a class, i.e. add to what can be done with its objects. There are two main ways in which a class B can extend the functionality of a class A: (a) adding new methods (b) widening the range of legal inputs to an existing method In order for a class user to take advantage of (a), it must have a reference of type B. You can't call these new methods through a reference of type A. To be sound, (b) should be equally subject to this requirement. It might be Walter's decision that, in D, (b) is going to continue to be exempt from this requirement. But then it's a WONTFIX. But otherwise, it's reasonable that some people may want (b) to be subject to the requirement, while others may want it to be exempt from it. It's an open matter of debate, therefore whatever this issue is, it certainly isn't INVALID. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 Walter Bright changed: What|Removed |Added Status|REOPENED|RESOLVED Resolution||INVALID --- Comment #22 from Walter Bright 2012-05-03 17:49:32 PDT --- Please stop reopening this. > If you mean whether a given call is legal, then you could by the same argument insist that called method names must be resolved in the context of the virtual type. And they are. It's what the vtbl[] is for. > (b) is going to continue to be exempt from this requirement. You cannot widen the requirements of a function without providing an override of it. A.foo() cannot be called with the widened requirements of B.foo() - B.foo() gets called. That's why it can be overridden. IT WORKS CORRECTLY. The virtualness of the contracts is directly connected to the virtualness of the function calls. As for the design decision on this, the decision was (and is) to implement classic OOP. It is theoretically sound. This is well trod and (I thought) well understood territory. As Andrei pointed out, it is not open for debate what OOP is. I realize I am not very good at explaining this. I seriously recommend reading Meyer's book Object Oriented Programming. It's only $5.99. If we try and implement alternate and incorrection notions of OOP, D will be considered a lightweight language run by amateurs. It is entirely possible that: 1. I have seriously misunderstood OOP (I have made more than my share of such mistakes before). 2. The OOP community has got it all wrong. As evidence for (1), is there any OOP language that does it these other ways? Spec# does not, as Andrei researched and pointed out. For (2), you've got a high bar to overcome, and certainly have an opportunity for a groundbreaking academic paper. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #23 from Stewart Gordon 2012-05-03 18:21:44 PDT ---
(In reply to comment #22)
>> If you mean whether a given call is legal, then you could by the
>> same argument insist that called method names must be resolved in
>> the context of the virtual type.
>
> And they are. It's what the vtbl[] is for.
???
class A {}
class B : A {
void foo() {}
}
void main() {
A a = new B;
a.foo();
}
You're claiming that this code is legal, and the penultimate line resolves to
B's foo method???
>> (b) is going to continue to be exempt from this requirement.
>
> You cannot widen the requirements of a function without providing
> an override of it. A.foo() cannot be called with the widened
> requirements of B.foo() - B.foo() gets called. That's why it can
> be overridden.
The concept of overriding in OOP as I've been brought up to understand it
applies to what the method does, a quite different concept from what are legal
inputs to it.
> As for the design decision on this, the decision was (and is) to
> implement classic OOP. It is theoretically sound. This is well
> trod and (I thought) well understood territory. As Andrei pointed
> out, it is not open for debate what OOP is.
I'm surprised that the classic OOP spec covers the behaviour of contracts at
all. But maybe I just need to read up on it.
> As evidence for (1), is there any OOP language that does it these
> other ways? Spec# does not, as Andrei researched and pointed out.
> For (2), you've got a high bar to overcome, and certainly have an
> opportunity for a groundbreaking academic paper.
At least I seem to have three potential co-authors already
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #24 from Walter Bright 2012-05-03
18:50:03 PDT ---
(In reply to comment #23)
> (In reply to comment #22)
> >> If you mean whether a given call is legal, then you could by the
> >> same argument insist that called method names must be resolved in
> >> the context of the virtual type.
> >
> > And they are. It's what the vtbl[] is for.
>
> ???
>
> class A {}
>
> class B : A {
> void foo() {}
> }
>
> void main() {
> A a = new B;
> a.foo();
> }
>
> You're claiming that this code is legal, and the penultimate line resolves to
> B's foo method???
No, I'm not. This thread is about overriding, not introducing, functions.
> I'm surprised that the classic OOP spec covers the behaviour of contracts at
> all. But maybe I just need to read up on it.
Betrand Meyer's Object Oriented Programming. You can get it on amazon for
$5.99. It's the definitive classic on the topic.
The behavior with contracts is just another aspect of the contravariance and
covariance of derived objects.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #25 from Stewart Gordon 2012-05-03 19:02:13 PDT --- (In reply to comment #24) > No, I'm not. This thread is about overriding, not introducing, functions. It's about introducing new legal inputs to a function. Which is conceptually more like introducing a new function than overriding an existing function. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #26 from deadalnix 2012-05-04 01:46:25 PDT --- (In reply to comment #22) > You cannot widen the requirements of a function without providing an override > of it. A.foo() cannot be called with the widened requirements of B.foo() - > B.foo() gets called. That's why it can be overridden. IT WORKS CORRECTLY. The > virtualness of the contracts is directly connected to the virtualness of the > function calls. > > As for the design decision on this, the decision was (and is) to implement > classic OOP. It is theoretically sound. This is well trod and (I thought) well > understood territory. As Andrei pointed out, it is not open for debate what > OOP > is. No it isn't. OOP doesn't say anything about contracts. The concept of contract is different and the question here is how both interact in a specific corner case. > I realize I am not very good at explaining this. I seriously recommend reading > Meyer's book Object Oriented Programming. It's only $5.99. Is that book handle the corner case we are talking about here ? If it does, I'd be interested in what is the reasoning. The fact is that all document I read at this point do not say anything about this. > If we try and implement alternate and incorrection notions of OOP, D will be > considered a lightweight language run by amateurs. > I do agree, but once again, OOP isn't about contracts. > It is entirely possible that: > > 1. I have seriously misunderstood OOP (I have made more than my share of such > mistakes before). > > 2. The OOP community has got it all wrong. > You perfectly know that both are unlikely. Stating this avoid any interesting debate. As for now, we have 25 comment, and not once mention any argument in favor of keeping the standard behavior instead of the proposed one. > As evidence for (1), is there any OOP language that does it these other ways? > Spec# does not, as Andrei researched and pointed out. For (2), you've got a > high bar to overcome, and certainly have an opportunity for a groundbreaking > academic paper. I read many paper on the subject. None was covering the corner case we are talking about here. Without this corner case, both solutions satisfy requirements. However, the chosen one is simpler (in contract can simply be added to the function body). I'd be happy to see ONE argument on favor of the current behavior. Everybody is doing it isn't a valid argument. We are D, we know everybody is using C++ and PHP (among others), and we do also know that such languages are horribly crippled by all sort of crazyness. Everybody is doing it isn't an argument. PS: Note that in case of Spec#, the decision is made to DISALLOW override of in contracts. In such a situation, both behavior proposed in this thread are equivalent, and so, it is not a relevant example. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #27 from Andrei Alexandrescu 2012-05-04 04:03:36 PDT --- (In reply to comment #26) > No it isn't. OOP doesn't say anything about contracts. The concept of contract > is different and the question here is how both interact in a specific corner > case. Walter's explanation creates confusion because he uses the wrong vocabulary (i.e. OOP instead of Design by Contract). > > I realize I am not very good at explaining this. I seriously recommend > > reading > > Meyer's book Object Oriented Programming. It's only $5.99. > > Is that book handle the corner case we are talking about here ? Yes. There's another book on the subject called "Design by Contract, by Example". I wouldn't recommend it as a good book in general but it does teach the topic. > If it does, I'd > be interested in what is the reasoning. Well it's not all that reasonable to expect someone to essentially copy the text from the book or summarize it for you. > The fact is that all document I read at > this point do not say anything about this. It means you are reading the wrong documents. It takes literally under a minute to find relevant documents all over. > > As evidence for (1), is there any OOP language that does it these other > > ways? > > Spec# does not, as Andrei researched and pointed out. For (2), you've got a > > high bar to overcome, and certainly have an opportunity for a groundbreaking > > academic paper. > > I read many paper on the subject. None was covering the corner case we are > talking about here. Without this corner case, both solutions satisfy > requirements. However, the chosen one is simpler (in contract can simply be > added to the function body). There's no reason to doubt you are telling the truth, so this must be quite an interesting case of confirmation bias as you seem to have read only what doesn't infirm your hypothesis and glossed over everything that does. As an example, google for "design by contract" inheritance The literally FIRST hit takes to a slide deck, see http://goo.gl/544fU. There there is theory and examples on how contracts work. > I'd be happy to see ONE argument on favor of the current behavior. Everybody > is > doing it isn't a valid argument. It's a very valid argument. DbC is established. People learn about DbC from various places and they come to apply it in D. They'd be surprised and annoyed that D doesn't do what it's supposed to do. There are of course other arguments, which you can find in the literature. This is not the time and place for a course in DbC. > We are D, we know everybody is using C++ and > PHP (among others), and we do also know that such languages are horribly > crippled by all sort of crazyness. Everybody is doing it isn't an argument. On the other hand many are also doing some good things so gratuitously not doing them doesn't help, either. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #28 from Don 2012-05-04 04:48:20 PDT --- (In reply to comment #27) > (In reply to comment #26) > There's no reason to doubt you are telling the truth, so this must be quite an > interesting case of confirmation bias as you seem to have read only what > doesn't infirm your hypothesis and glossed over everything that does. > > As an example, google for > > "design by contract" inheritance > > The literally FIRST hit takes to a slide deck, see http://goo.gl/544fU. There > there is theory and examples on how contracts work. Andrei, those slides don't address the issue at all. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #29 from Andrei Alexandrescu 2012-05-04
05:35:12 PDT ---
(In reply to comment #28)
> > The literally FIRST hit takes to a slide deck, see http://goo.gl/544fU.
> > There
> > there is theory and examples on how contracts work.
>
> Andrei, those slides don't address the issue at all.
The issue as exemplified herein is:
class A {
void foo(int x) in { assert(x > 0); } body {}
}
class B : A {
void foo(int x) in { assert(x > -2); } body {}
}
void fizzbuzz(A a) {
a.foo(-1);
}
The question is, why does the code work when A's contract is in fact violated.
Slide 22-10 in that deck gives as example a method invert(). The base class has
precondition epsilon >= 10^(– 6) and the derived class has precondition epsilon
>= 10^(– 20). The surrounding slides explain rather copiously how a call to
invert against the derived class works even though the precondition of the base
class is violated (e.g. by passing epsilon = 10^(– 10). The example given in
the slides has a straightforward correspondence to the one above.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #30 from Don 2012-05-04 05:57:39 PDT ---
(In reply to comment #29)
> (In reply to comment #28)
> > > The literally FIRST hit takes to a slide deck, see http://goo.gl/544fU.
> > > There
> > > there is theory and examples on how contracts work.
> >
> > Andrei, those slides don't address the issue at all.
>
> The issue as exemplified herein is:
>
> class A {
> void foo(int x) in { assert(x > 0); } body {}
> }
>
> class B : A {
> void foo(int x) in { assert(x > -2); } body {}
> }
>
> void fizzbuzz(A a) {
> a.foo(-1);
> }
>
> The question is, why does the code work when A's contract is in fact violated.
> Slide 22-10 in that deck gives as example a method invert(). The base class
> has
> precondition epsilon >= 10^(– 6) and the derived class has precondition
> epsilon
> >= 10^(– 20). The surrounding slides explain rather copiously how a call to
> invert against the derived class works even though the precondition of the
> base
> class is violated (e.g. by passing epsilon = 10^(– 10). The example given in
> the slides has a straightforward correspondence to the one above.
You are making a massive assumption here, which I don't see in the slides. The
assumption is that fizzbuzz gets access to B's weakened precondition.
I've looked all over the Eiffel website and haven't seen anything which implies
that. Rather, everything I read implies that it's a contract -- it's the
clients responsibility to ensure that the precondition is satisfied. fizzbuzz
doesn't have a contract with B, it doesn't even know that B exists.
fizzbuzz() clearly has a bug. It will fail if given an A which isn't actually a
B.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #31 from Andrei Alexandrescu 2012-05-04 06:21:14 PDT --- (In reply to comment #30) > You are making a massive assumption here, which I don't see in the slides. The > assumption is that fizzbuzz gets access to B's weakened precondition. > I've looked all over the Eiffel website and haven't seen anything which > implies > that. Rather, everything I read implies that it's a contract -- it's the > clients responsibility to ensure that the precondition is satisfied. fizzbuzz > doesn't have a contract with B, it doesn't even know that B exists. I understand the distinction, and how the slides doesn't make it clear that the precondition is dynamically bound. In fact the author found it so obvious as to be unnecessary to mention (generally in the OOP world all methods are dynamically bound unless expressly noted otherwise; C++ is an anomaly). The second hit, http://goo.gl/5r7BF, clarifies with the diagrams on slides 17, 18, 20 and with the associated text that client code interacts with the base class only. The ultimate proof would be to read Meyer's book on DbC (or the other one) and/or download the Eiffel compiler and compile an example. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #32 from Stewart Gordon 2012-05-04 10:38:33 PDT --- (In reply to comment #30) > fizzbuzz() clearly has a bug. It will fail if given an A which isn't actually > a > B. Exactly. fizzbuzz is calling a method of A, not a method of B. As such, as I've already said, it must conform to A's API, but it is failing to do so. (In reply to comment #31) > I understand the distinction, and how the slides doesn't make it clear that > the > precondition is dynamically bound. In fact the author found it so obvious as > to > be unnecessary to mention So it could have been just an oversight for all we know. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #33 from Walter Bright 2012-05-04
11:42:40 PDT ---
(In reply to comment #32)
> (In reply to comment #30)
> > fizzbuzz() clearly has a bug. It will fail if given an A which isn't
> > actually a
> > B.
>
> Exactly. fizzbuzz is calling a method of A, not a method of B. As such, as
> I've already said, it must conform to A's API, but it is failing to do so.
First off, if fizzbuzz() is passed an A, then it will (correctly) fail. Where's
the bug in the contract design? Secondly, the -1 may not be a literal, it may
be a value computed from B, as in:
class A {
void foo(int x) in { assert(x > 0); } body {}
int bar() { return 1; }
}
class B : A {
void foo(int x) in { assert(x > -2); } body {}
int bar() { return -1; }
}
void fizzbuzz(A a) {
a.foo(bar());
}
So, clearly is NOT required that a.foo(arg) pass A.foo's contract.
The design of OOP and contracts is sound. Correct programs will pass, and
incorrect programs will fail. I don't see any "corner cases" otherwise.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #34 from Stewart Gordon 2012-05-04 13:27:50 PDT ---
(In reply to comment #33)
OK, so there's this issue. It may also be a documented guarantee that the
return value from bar is a valid argument for foo.
But you could still argue that the call is in breach of A's API and therefore
the code is incorrect. To be correct, the in contract for A.foo would have to
be something like
in { assert(x > 0 || x == bar()); }
But since enforcing this now is a potentially breaking change, I can now see a
case for leaving the behvaiour as it is.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #35 from Walter Bright 2012-05-04
13:41:50 PDT ---
(In reply to comment #34)
> But you could still argue that the call is in breach of A's API and therefore
> the code is incorrect.
Again, this is NOT true. The type of the argument is not statically A, it is a
polymorphic type A.
If an instance of A is passed, then the call to foo(-1) will fail. Please try
it and see for yourself. There is no hole in the system.
> To be correct, the in contract for A.foo would have to
> be something like
>
> in { assert(x > 0 || x == bar()); }
>
> But since enforcing this now is a potentially breaking change, I can now see a
> case for leaving the behvaiour as it is.
You are still seeing this as a bug in the OOP design. It is not. The design is
sound and correct.
If you still disagree, please write a code sample that asserts when it should
not, or passes when it must not, compile it and run it, and post it here.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #36 from Stewart Gordon 2012-05-04 13:49:11 PDT --- (In reply to comment #35) > Again, this is NOT true. The type of the argument is not statically > A, it is a polymorphic type A. Why do you consider the contracts of a method to be NOT part of the API? Because Bertrand considers it so, or for some other reason? > If an instance of A is passed, then the call to foo(-1) will fail. > Please try it and see for yourself. I never doubted that. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #37 from Walter Bright 2012-05-04 14:13:50 PDT --- (In reply to comment #36) > (In reply to comment #35) > > > Again, this is NOT true. The type of the argument is not statically > > A, it is a polymorphic type A. > > Why do you consider the contracts of a method to be NOT part of the API? This is not what I am considering. I am saying that A is a polymorphic type, not a static type. The contracts that apply depend on the runtime polymorphic type, not the static type. > Because Bertrand considers it so, or for some other reason? I am not using argument by authority. Meyer explains it quite well, step by step, in his book I recommended to you. The behavior is an inevitable consequence of the fundamental principles of OOP. That is why it is not a matter of opinion. > > If an instance of A is passed, then the call to foo(-1) will fail. > > Please try it and see for yourself. > > I never doubted that. Then I am lost as to what you think is broken in the design. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #38 from Stewart Gordon 2012-05-04 14:30:40 PDT --- (In reply to comment #37) > Then I am lost as to what you think is broken in the design. In how many different ways does the same thing need to be explained to you before you understand it? If a subclass introduces a new method, that new method doesn't exist from the base class's point of view. In the same way, if a subclass introduces new legal arguments to a method, those new legal arguments don't exist from the base class's point of view. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #39 from Walter Bright 2012-05-04 14:46:11 PDT --- Please write a piece of code that asserts when it should not, or passes when it should not, compile it, verify this incorrect behavior, and post it here. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #40 from Stewart Gordon 2012-05-04 14:52:44 PDT --- (In reply to comment #39) > Please write a piece of code that asserts when it should not, or passes when > it > should not, compile it, verify this incorrect behavior, and post it here. Timon has already done this and posted it in the description when filing this report in the first place. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #41 from Walter Bright 2012-05-04 15:18:08 PDT --- (In reply to comment #40) > (In reply to comment #39) > > Please write a piece of code that asserts when it should not, or passes > > when it > > should not, compile it, verify this incorrect behavior, and post it here. > > Timon has already done this and posted it in the description when filing this > report in the first place. Example #1 expects behavior based on the static type, which is not polymorphic OOP at all. Of course x.foo() should check B's widened interface, because: x is a B! The example's rationale is completely invalid. Please read Meyer's book. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #42 from Stewart Gordon 2012-05-04 15:27:45 PDT --- (In reply to comment #41) > Example #1 expects behavior based on the static type, which is not polymorphic > OOP at all. True, but it is what this enhancement request is all about. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #43 from Walter Bright 2012-05-04 17:40:19 PDT --- (In reply to comment #42) > True, but it is what this enhancement request is all about. Breaking correct OOP behavior is not an enhancement. It will not break existing wrong-but-just-happens-to-work programs, it will break *correct* programs. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #44 from Stewart Gordon 2012-05-04 17:50:19 PDT --- (In reply to comment #43) > (In reply to comment #42) >> True, but it is what this enhancement request is all about. > > Breaking correct OOP behavior is not an enhancement. But going by comment 26, there is no breakage of correct OOP behaviour involved. So how is this relevant? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #45 from Walter Bright 2012-05-04 18:18:11 PDT --- (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. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #46 from Don 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.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #47 from Walter Bright 2012-05-05 02:02:48 PDT --- (In reply to comment #46) > Now, change F from a struct to a class. We believe that the code should still > fail to compile. A theorem prover could not produce a compile time error, because it could not prove that f is actually an F, and not of a class derived from F. OOP is runtime polymorphism, not compile time. A struct type is fundamentally different from a class type. And lastly, your request is quite different from Example #1, which is asserting that the contract for A.foo() must always pass, even if it's calling B.foo(). I know I sound like a broken record, but please read Meyer's book. He shows how the behavior of contracts is a derived consequence from OOP principles. It is not a separate invention with separate rules. Hence it is not a matter of belief - it is a matter of proof. --- Comment #48 from Walter Bright 2012-05-05 02:03:05 PDT --- (In reply to comment #46) > Now, change F from a struct to a class. We believe that the code should still > fail to compile. A theorem prover could not produce a compile time error, because it could not prove that f is actually an F, and not of a class derived from F. OOP is runtime polymorphism, not compile time. A struct type is fundamentally different from a class type. And lastly, your request is quite different from Example #1, which is asserting that the contract for A.foo() must always pass, even if it's calling B.foo(). I know I sound like a broken record, but please read Meyer's book. He shows how the behavior of contracts is a derived consequence from OOP principles. It is not a separate invention with separate rules. Hence it is not a matter of belief - it is a matter of proof. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #47 from Walter Bright 2012-05-05 02:02:48 PDT --- (In reply to comment #46) > Now, change F from a struct to a class. We believe that the code should still > fail to compile. A theorem prover could not produce a compile time error, because it could not prove that f is actually an F, and not of a class derived from F. OOP is runtime polymorphism, not compile time. A struct type is fundamentally different from a class type. And lastly, your request is quite different from Example #1, which is asserting that the contract for A.foo() must always pass, even if it's calling B.foo(). I know I sound like a broken record, but please read Meyer's book. He shows how the behavior of contracts is a derived consequence from OOP principles. It is not a separate invention with separate rules. Hence it is not a matter of belief - it is a matter of proof. --- Comment #48 from Walter Bright 2012-05-05 02:03:05 PDT --- (In reply to comment #46) > Now, change F from a struct to a class. We believe that the code should still > fail to compile. A theorem prover could not produce a compile time error, because it could not prove that f is actually an F, and not of a class derived from F. OOP is runtime polymorphism, not compile time. A struct type is fundamentally different from a class type. And lastly, your request is quite different from Example #1, which is asserting that the contract for A.foo() must always pass, even if it's calling B.foo(). I know I sound like a broken record, but please read Meyer's book. He shows how the behavior of contracts is a derived consequence from OOP principles. It is not a separate invention with separate rules. Hence it is not a matter of belief - it is a matter of proof. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #49 from Stewart Gordon 2012-05-05 04:40:48 PDT --- (In reply to comment #47) > (In reply to comment #46) > > Now, change F from a struct to a class. We believe that the code should > > still > > fail to compile. > > A theorem prover could not produce a compile time error, because it could not > prove that f is actually an F, and not of a class derived from F. You have completely ignored the whole point of this request, which has been explained to you by four of us several times over. > OOP is runtime polymorphism, not compile time. A struct type is fundamentally > different from a class type. Runtime polymorphism is about overriding behaviour, not overriding legality. > And lastly, your request is quite different from Example #1, which is > asserting > that the contract for A.foo() must always pass, even if it's calling B.foo(). What are you talking about? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #50 from deadalnix 2012-05-05 05:04:07 PDT ---
(In reply to comment #33)
> (In reply to comment #32)
> > (In reply to comment #30)
> > > fizzbuzz() clearly has a bug. It will fail if given an A which isn't
> > > actually a
> > > B.
> >
> > Exactly. fizzbuzz is calling a method of A, not a method of B. As such, as
> > I've already said, it must conform to A's API, but it is failing to do so.
>
> First off, if fizzbuzz() is passed an A, then it will (correctly) fail.
> Where's
> the bug in the contract design? Secondly, the -1 may not be a literal, it may
> be a value computed from B, as in:
>
>
> class A {
> void foo(int x) in { assert(x > 0); } body {}
> int bar() { return 1; }
> }
>
> class B : A {
> void foo(int x) in { assert(x > -2); } body {}
> int bar() { return -1; }
> }
>
> void fizzbuzz(A a) {
> a.foo(bar());
> }
>
> So, clearly is NOT required that a.foo(arg) pass A.foo's contract.
>
> The design of OOP and contracts is sound. Correct programs will pass, and
> incorrect programs will fail. I don't see any "corner cases" otherwise.
This piece of code is good for an horror museum.
If bar is a valid argument for foo, then A should have the following definition
:
class A {
void foo(int x) in { assert(x > 0); } body {}
int bar() out(result) { assert( result > 0); } body { return 1; }
}
And, with such a definition, out contract would prevent B.bar to return -1 .
BTW, I found this PDF on Meyer's website :
se.ethz.ch/~meyer/publications/computer/contract.pdf . It seems that he decided
to publish the part of the book that is relevant to us online. I'm reading it
right now.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #51 from deadalnix 2012-05-05 06:22:21 PDT --- (In reply to comment #49) > Runtime polymorphism is about overriding behaviour, not overriding legality. > This is, indeed, the whole essence of the problem. (In reply to comment #48) > And lastly, your request is quite different from Example #1, which is > asserting > that the contract for A.foo() must always pass, even if it's calling B.foo(). > I'm afraid this explains why we are not getting anywhere in this discussion. The whole proposal is, and have always been that one. Read again example code I've posted and which check is performed in which case. I have read Mayer's document about contract and OOP, and I want to comment here the explanations given by Meyer himself. Quoted passage are from the book. Mayer have a very similar example to the one I gave above. You have classes A and B inheriting from A. A define a method r with an in contract, that B override. A variable u of type A is used in method X. You can map as this : r <=> foo, u <=> a and X <=> fizzbuzzA « To ascertain the properties of the call u.r, the author of X can only look at the contract for r in A. Yet, because of dynamic binding, A may subcontract the execution of r to B, and it is B’s contract that will be applied. » Here, Meyer is stating HOW thing work before it explain WHY. Hence, the whole stuff is to show how this specific implementation satisfy certain properties. Let see what are these properties and what is the situation with the new proposed behavior. « How do you avoid “fooling” X in the process? There are two ways B could violate its prime contractor’s promises: - B could make the precondition stronger, raising the risk that some calls that are correct from x’s viewpoint (they satisfy the original client obligations) will not be handled properly. » I omitted the second one as it is about out contract so off topic here. the constraint expressed here is respected by both current solution, and proposed solution. « None of this, then, is permitted. But the reverse changes are of course legitimate. A redeclaration may weaken the original’s precondition or it may strengthen the postcondition. » Again, both proposals allow this. « Redeclaration. for all the power it brings to software development. is not a way to turn a routine into something completely different. The new version must remain compatible with the original specification. although it may improve on it. The noted rules express this precisely. » Meyer is right. His rules express this. But proposed rules express this too. He then conclude « In this way. the new precondition is guaranteed to be weaker than or equal to the originals, and the new postcondition is guaranteed to be stronger than or equal to the originals. » Again according to Meyer's argumentation, both behavior are corrects. It appears (and I have read the chapter several times to make sure I'm not missing something) that Meyer's doesn't provide any argument about our special case here. I'm sorry, but this reading can't close the discussion. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #52 from Andrei Alexandrescu 2012-05-05 08:54:17 PDT --- (In reply to comment #51) > I'm sorry, but this reading can't close the discussion. I think it does. The proposed behavior does not allow this: "None of this, then, is permitted. But the reverse changes are of course legitimate. A redeclaration may weaken the original’s precondition or it may strengthen the postcondition. Changes of either kind mean that the subcon- tractor does a better job than the original contractor-which there is no reason to prohibit." Doing a better job is succeeding where the parent method would have failed its precondition. It all boils down to the fact that it's natural to have methods that can't work in the parent but do work in the child. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #53 from deadalnix 2012-05-05 08:58:21 PDT ---
(In reply to comment #52)
> (In reply to comment #51)
> > I'm sorry, but this reading can't close the discussion.
>
> I think it does. The proposed behavior does not allow this:
>
> "None of this, then, is permitted. But the reverse changes are of course
> legitimate. A redeclaration may weaken the original’s precondition or it may
> strengthen the postcondition. Changes of either kind mean that the subcon-
> tractor does a better job than the original contractor-which there is no
> reason
> to prohibit."
>
And indeed, it is not prohibited.
> Doing a better job is succeeding where the parent method would have failed its
> precondition. It all boils down to the fact that it's natural to have methods
> that can't work in the parent but do work in the child.
It is stated (quoting myself) that :
« fizzbuzzB(B b) {
b.foo(); // (A.foo OR B.foo)'s in contract is valid
} »
Which exactly the behavior you talk about.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #54 from Stewart Gordon 2012-05-05 09:21:02 PDT --- (In reply to comment #52) > Doing a better job is succeeding where the parent method would have failed its > precondition. It all boils down to the fact that it's natural to have methods > that can't work in the parent but do work in the child. And to take advantage of this, one would deal with the child directly. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 Walter Bright changed: What|Removed |Added Status|RESOLVED|REOPENED Resolution|INVALID | Severity|enhancement |normal --- Comment #55 from Walter Bright 2012-05-05 17:27:24 PDT --- Mea culpa. I read Meyer's book again. Chapter 16.1 "Cutting out the middleman" pg. 575 says: "A client of MATRIX must satisfy the original (stronger) precondition, and may only expect the original (weaker) postcondition; even if its request gets served dynamically by NEW_MATRIX it has no way of benefiting from the broader tolerance of inputs and tighter precision of results. To get this improved specification it must declare the matric to be of type NEW_MATRIX, thereby losing access to other implementations represented by descendants of MATRIX that are not also descendants of NEW_MATRIX." (MATRIX is the base class, NEW_MATRIX is the derived class.) So I'm reopening it as a normal bug. Unfortunately, I do not currently see a reasonable way of implementing this. Fortunately, as is it does not inhibit correct programs, it only accepts some invalid ones. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #56 from Don 2012-05-06 00:36:04 PDT ---
(In reply to comment #55)
> Mea culpa.
>
> I read Meyer's book again. Chapter 16.1 "Cutting out the middleman" pg. 575
> says:
>
> "A client of MATRIX must satisfy the original (stronger) precondition, and may
> only expect the original (weaker) postcondition; even if its request gets
> served dynamically by NEW_MATRIX it has no way of benefiting from the broader
> tolerance of inputs and tighter precision of results. To get this improved
> specification it must declare the matric to be of type NEW_MATRIX, thereby
> losing access to other implementations represented by descendants of MATRIX
> that are not also descendants of NEW_MATRIX."
>
> (MATRIX is the base class, NEW_MATRIX is the derived class.)
>
> So I'm reopening it as a normal bug.
>
> Unfortunately, I do not currently see a reasonable way of implementing this.
> Fortunately, as is it does not inhibit correct programs, it only accepts some
> invalid ones.
I think implementation is simpler than what happens at present. You need a
static function thunk for each virtual function with a precondition.
For example:
class A {
int foo(int n) in { assert(n >0); } body { return n; }
}
class B {
int foo(int n) { return n+1; } // no change to precondition
}
class C {
int foo(int n) in { assert(n > -10 && n<-6); } body { return n+2; }
becomes (I've put 'virtual' in to make things clearer):
class A {
static void foo_in(A x) { assert(n>0); }
virtual int foo(int n) { foo_in(this, n); return foo_body(n); }
virtual int foo_body(int n) { return n; }
}
class B {
virtual int foo_body(int n) { return n+1; }
}
class C {
static void foo_in(C x, int n) { assert(n > -10 && n<-6); }
virtual int foo(int n ) {
if (C.foo_in(this, n)) return foo_body(n); // passed C's precondition
return A.foo(n); // failed, try A's precondition
}
virtual int foo_body(int n) { return n+2; }
}
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #57 from deadalnix 2012-05-06 02:20:47 PDT --- (In reply to comment #55) > So I'm reopening it as a normal bug. > Thank you ! > Unfortunately, I do not currently see a reasonable way of implementing this. > Fortunately, as is it does not inhibit correct programs, it only accepts some > invalid ones. That is not this complicated. you need a final function that check the in contract, then call another virtual function that actually execute the function body and the out contract. With such a configuration, the in contract is checked and only then the virtual dispatch is done. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #59 from deadalnix 2012-05-06 03:27:45 PDT --- (In reply to comment #58) > It's not that simple. Several considerations have to be met: > > 1. Because of struct construction/destruction, you really only want to > construct the parameter list *once*, but you're calling two functions with the > same parameter list. > Arguments should really be const in contracts. And if they are not modified (and considering that argument are the same for in contract function and real function) it is probably doable to jump right into the implementation function just after the prolog. > 2. Variadic functions mean that one function cannot forward to another one > using standard functions. (Perhaps a dirty magic thunk can work.) > Again, I think jumping right into the function can do the trick. > 3. The presence or absence of contracts must not change the ABI of the > function. > That one seem really difficult. An alternative would be to do 2 function calls, one for in contract and one for the function body. Another option is to consider contract as being part of the declaration and so cannot be opaque. > 4. The virtual table must be unchanged. > With proposed solution it will, even if a direct call throw the virtual table would skip the in contract. > 5. It's not so practical to jump into the middle of another function - things > just aren't designed that way. > Already did that. This isn't something you want to do every day, but it doable. > 6. The caller now has to be aware of contracts in the called function, this > was > never necessary before. Indeed, the caller now has to be aware of the existence of in contracts. This is required if you want to check contract according to caller's type and not real type. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #60 from Andrei Alexandrescu 2012-05-06 19:48:55 PDT --- This has been some significant pwning of Walter and myself, and I think there is a larger lesson here we should learn. We essentially operated from vague memories instead of actually going back and revisit the sources. This must be how some dogma is born - an imprecise and incorrect recollection of some assumption that becomes petrified. What I think we should do going forward is to make sure we state and document our assumptions instead of relying on rote recollection. The DbC-related documentation and language specification should contain chapter and page of Meyer's work. There's a good reason why all academic work makes sure cites all of its sources, and even that is liable to mistakes of the kind we've done. Thanks to all who have pursued this matter. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #61 from Stewart Gordon 2012-05-07 03:58:47 PDT ---
(In reply to comment #58)
> It's not that simple. Several considerations have to be met:
>
> 1. Because of struct construction/destruction, you really only
> want to construct the parameter list *once*, but you're calling two
> functions with the same parameter list.
Can't this be solved by simply making all struct parameters to the in/out
functions ref?
(I've never been sure about this struct construction/destruction business
anyway. Struct constructors are nice, but I must've thought at a time that
part of the design of D is that structs can always safely be just bit-copied.)
> 2. Variadic functions mean that one function cannot forward to
> another one using standard functions. (Perhaps a dirty magic thunk
> can work.)
>
> 3. The presence or absence of contracts must not change the ABI of
> the function.
>
> 4. The virtual table must be unchanged.
I assume these were part of the reason for using nested functions to implement
contract inheritance. 2 is indeed something that needs to be considered. But
is forwarding the arguments any more difficult than putting the arguments onto
the stack in the first place?
As for 3 and 4, the in/out functions don't need to be virtual as far as I can
see, so this shouldn't cause much difficulty.
> 5. It's not so practical to jump into the middle of another
> function - things just aren't designed that way.
>
> 6. The caller now has to be aware of contracts in the called
> function, this was never necessary before.
I think this is a good thing, since it enables the user of a library to switch
on/off in contract checking without having to rebuild the library.
(In reply to comment #56)
> class A {
> static void foo_in(A x) { assert(n>0); }
> virtual int foo(int n) { foo_in(this, n); return foo_body(n); }
> virtual int foo_body(int n) { return n; }
> }
foo needs to be non-virtual - otherwise you're implementing dynamic binding,
which we already have, not static binding.
Indeed, it should be something like this
class A {
void foo_in(int n) { assert(n>0); }
int foo_dbc(int n) { foo_in(this, n); return foo(n); }
virtual int foo(int n) { return n; }
}
then a call to foo would translate to a call to foo_dbc when compiling in
non-release mode. This also has the advantage of not changing the vtable
layout.
The difficulty is that the library might have been built in release mode, with
foo_in and foo_dbc absent. Can we get around this by treating them as nullary
templates, so they are compiled/linked in according to usage?
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #62 from deadalnix 2012-05-07 04:43:25 PDT --- (In reply to comment #60) > This has been some significant pwning of Walter and myself, and I think there > is a larger lesson here we should learn. > Quoting yourself � Mistakes happen to the best of us. �. Don't worry, I think your reaction is very safe, and I'm happy to see D evolving that way. Changing how the language work must be done only if strong arguments are made. Providing documentation on language design decision is surely a way to improve the current state of things. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #63 from Walter Bright 2012-05-07
08:29:21 PDT ---
(In reply to comment #61)
> (In reply to comment #58)
> > It's not that simple. Several considerations have to be met:
> >
> > 1. Because of struct construction/destruction, you really only
> > want to construct the parameter list *once*, but you're calling two
> > functions with the same parameter list.
>
> Can't this be solved by simply making all struct parameters to the in/out
> functions ref?
Losing all C ABI compatiblity in the process.
> I assume these were part of the reason for using nested functions to implement
> contract inheritance. 2 is indeed something that needs to be considered. But
> is forwarding the arguments any more difficult than putting the arguments onto
> the stack in the first place?
How do you forward a variadic function? You don't know what's on the stack to
forward.
> class A {
> void foo_in(int n) { assert(n>0); }
> int foo_dbc(int n) { foo_in(this, n); return foo(n); }
> virtual int foo(int n) { return n; }
> }
>
> then a call to foo would translate to a call to foo_dbc when compiling in
> non-release mode. This also has the advantage of not changing the vtable
> layout.
Again, you're pushing the parameters on the stack twice - and this won't work
for variadic functions.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #64 from deadalnix 2012-05-07 09:00:05 PDT --- (In reply to comment #63) > Again, you're pushing the parameters on the stack twice - and this won't work > for variadic functions. Why not jump in the function directly after the prolog and not push arguments twice on the stack ? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #65 from Walter Bright 2012-05-07 09:36:56 PDT --- (In reply to comment #64) > Why not jump in the function directly after the prolog and not push arguments > twice on the stack ? Not so easy given how back ends are designed. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #66 from Stewart Gordon 2012-05-07 10:32:33 PDT --- (In reply to comment #63) > > Can't this be solved by simply making all struct parameters to the in/out > > functions ref? > > Losing all C ABI compatiblity in the process. Contracts don't exist in C - so what's there to lose? > How do you forward a variadic function? You don't know what's on the stack to > forward. How do you implement a variadic function at all without knowing this? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #67 from Stewart Gordon 2012-05-07 10:48:26 PDT --- (In reply to comment #62) > Changing how the language work must be done only if strong arguments are made. Unless I've missed something, the language leaves this unspecified. So a compiler is free to do it either way. Though it would be better if it were specified. > Providing documentation on language design decision is surely a way to improve > the current state of things. Indeed, if all rationales scattered about the D docs were collected in one place, and a few more that we ought to have were added, I wonder how big this section would be. FTR, look at the PNG rationale page http://www.libpng.org/pub/png/spec/1.2/PNG-Rationale.html -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #68 from Walter Bright 2012-05-07 12:17:19 PDT --- (In reply to comment #66) > (In reply to comment #63) > > > Can't this be solved by simply making all struct parameters to the in/out > > > functions ref? > > > > Losing all C ABI compatiblity in the process. > > Contracts don't exist in C - so what's there to lose? 1. pass by ref is semantically very different from pass by value. It is necessary to support both. 2. D supports using C calling conventions, including having contracts on functions callable from C. > > How do you forward a variadic function? You don't know what's on the stack > > to > > forward. > > How do you implement a variadic function at all without knowing this? See printf, an example of where such knowledge is known by the programmer, not the language semantics. Just for fun, I suggest you try to implement a "myprintf" function which forwards all its arguments to printf. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #69 from Stewart Gordon 2012-05-07 12:26:47 PDT --- (In reply to comment #68) > 1. pass by ref is semantically very different from pass by value. It is > necessary to support both. The function that implements a contract is an internal thing. If you can implement said function to receive the struct by value, you can equally implement it to receive the struct by reference. > 2. D supports using C calling conventions, including having contracts on > functions callable from C. But the contract itself doesn't need to be callable from C. Only the overall function does. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
David Piepgrass changed:
What|Removed |Added
CC||qwertie...@gmail.com
--- Comment #70 from David Piepgrass 2012-07-08 14:27:53
PDT ---
I must say, I would be entirely opposed to fixing this "bug". As far as I can
see, the arguments of Timon and deadalnix have been entirely theoretical,
whereas it's not that hard to envision a situation where the user would fully
desire and expect the wider contract of B to apply even though the static type
is A.
Suppose that D did check *only* A's contract when calling into an A (that might
be a B). I bet that if contracts were widely and exactingly used, cases where
this causes trouble would pop up frequently. The main problem, I think, are
low-level "deputies" that provide functionality for higher-level clients.
For example, consider a collection that only allows items that match certain
constraints, but the constraints are eliminated in B:
// BTW I wanted to use an interface here, but I get
// "missing body { ... } after in or out"
// and then if I add a body, D complains that it is not abstract!
class A {
abstract void add(Item item)
in { assert(item.x > 0); } body {}
}
class B : A {
override void add(Item item) in {} body {}
}
struct Item { int x; }
Now suppose I write a function that helpfully adds a series of items to an A:
void addAll(A set, Item[] arr...) {
foreach(Item x; arr)
set.add(x);
}
Finally, a client creates a B and tries to add some items to it. That should be
okay, since B has no restrictions on the items:
B b = new B();
b.addAll(Item(-1), Item(-2), Item(-3));
Very few developers would consider this code to be in error. And if there is an
error, where is it?
P.S. Besides which, the implementation difficulties mentioned by Walter in
comment 58 are really big difficulties, that don't seem worth it for what
appears to be a minor behavior tweak.
P.P.S. in http://dlang.org/function.html, surely the syntax described in
"D-style Variadic Functions" is not the preferred technique since it isn't even
mentioned in TDPL book. Ergo, the "Typesafe Variadic Functions" section should
be first, and one of the two sections should explain to us why there are two
entirely different syntaxes!
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #71 from deadalnix 2012-07-08 14:50:57 PDT --- The error is in the fact that addAll isn't aware of B. You can solve that easily with metaprograming, or by overloading addAll for B. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #72 from timon.g...@gmx.ch 2012-07-08 14:58:07 PDT ---
(In reply to comment #70)
> I must say, I would be entirely opposed to fixing this "bug". As far as I can
> see, the arguments of Timon and deadalnix have been entirely theoretical,
It is irrelevant who made the arguments.
> whereas it's not that hard to envision a situation where the user would fully
> desire and expect the wider contract of B to apply even though the static type
> is A.
>
> Suppose that D did check *only* A's contract when calling into an A (that
> might
> be a B). I bet that if contracts were widely and exactingly used, cases where
> this causes trouble would pop up frequently. The main problem, I think, are
> low-level "deputies" that provide functionality for higher-level clients.
>
> For example, consider a collection that only allows items that match certain
> constraints, but the constraints are eliminated in B:
>
> // BTW I wanted to use an interface here, but I get
> // "missing body { ... } after in or out"
> // and then if I add a body, D complains that it is not abstract!
Yah, that's a long standing bug.
> class A {
> abstract void add(Item item)
> in { assert(item.x > 0); } body {}
> }
> class B : A {
> override void add(Item item) in {} body {}
> }
> struct Item { int x; }
>
> Now suppose I write a function that helpfully adds a series of items to an A:
>
> void addAll(A set, Item[] arr...) {
> foreach(Item x; arr)
> set.add(x);
> }
>
This function is clearly in error. You could do it like this:
class A {
abstract void add(Item item) in { assert(validate(item)); }
bool validate(Item item) const pure { return item.x > 0; }
}
class B : A {
override void add(Item item) {}
override bool validate(Item item) const pure { return true; }
}
void addAll(A set, Item[] arr...)in{
foreach(x; arr) assert(set.validate(x));
}body{
foreach(x; arr) set.add(x);
}
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #73 from timon.g...@gmx.ch 2012-07-08 15:08:47 PDT --- (In reply to comment #70) > > P.S. Besides which, the implementation difficulties mentioned by Walter in > comment 58 are really big difficulties, that don't seem worth it for what > appears to be a minor behavior tweak. > The reason why it is harder to implement is that it is more general. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #74 from Stewart Gordon 2012-07-08 15:59:47 PDT ---
(In reply to comment #72)
> (In reply to comment #70)
>> // BTW I wanted to use an interface here, but I get
>> // "missing body { ... } after in or out"
>> // and then if I add a body, D complains that it is not abstract!
>
> Yah, that's a long standing bug.
See issue 6549.
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #75 from David Piepgrass 2012-07-08 17:05:28 PDT --- > > I must say, I would be entirely opposed to fixing this "bug". As far as I > > can > > see, the arguments of Timon and deadalnix have been entirely theoretical, > > It is irrelevant who made the arguments. Relax, I didn't claim that it was relevant. Merely mentioning someone's name does not qualify as an ad-hominim attack. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857
--- Comment #76 from yebblies 2012-07-10 02:54:06 EST ---
(In reply to comment #55)
>
> Unfortunately, I do not currently see a reasonable way of implementing this.
> Fortunately, as is it does not inhibit correct programs, it only accepts some
> invalid ones.
I can't see any way to do it without changing the abi for virtual functions
with contracts.
But, if changing the abi was ok, I think something like this would work:
class A
{
void func(..., __in_contract_ptr)
{
void __nested_in_contract_A_func() { ... }
auto __in_contract = &__nested_in_contract_A_func;
__in_contract.ptr = ptr;
__in_contract();
...
}
}
class B : A
{
void func(..., __in_contract_ptr)
{
void __nested_in_contract_B_func() { ... }
auto __in_contract = &__nested_in_contract_B_func;
__in_contract.ptr = ptr;
__in_contract();
...
}
}
void main()
{
B b = new B();
b.func(..., &__nested_in_contract_B_func.ptr);
A a = b;
a.func(..., &__nested_in_contract_A_func.ptr);
}
--
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
--- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #77 from Stewart Gordon 2012-07-09 11:12:52 PDT --- (In reply to comment #76) > I can't see any way to do it without changing the abi for virtual functions > with contracts. What about my suggestion of comment 61? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 yebblies changed: What|Removed |Added CC||yebbl...@gmail.com --- Comment #78 from yebblies 2012-07-10 04:43:07 EST --- (In reply to comment #77) > (In reply to comment #76) > > I can't see any way to do it without changing the abi for virtual functions > > with contracts. > > What about my suggestion of comment 61? As Walter said, that requires argument forwarding, which introduces copying problems and doesn't work with variadics. The precondition needs to be evaluated in the context of the function. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #79 from Stewart Gordon 2012-07-09 15:22:23 PDT --- (In reply to comment #78) > As Walter said, that requires argument forwarding, which introduces copying > problems and doesn't work with variadics. I thought I'd debunked that, but you're right. By my proposal, user code would be calling either foo_dbc or foo depending on whether it's compiled in dev or release mode. And foo_dbc forwards to foo. But it does seem to be down to two problems with D's design: - structs aren't guaranteed to be safe to just bit-copy (this problem was introduced in D2) - we have variadics that are really just C's variadics with typeinfo added Something else I should've realised earlier: Why do D class methods need to be directly callable from C? (How does C code hold a reference to a D object, anyway?) Indeed, is even C++ designed to accommodate this? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #80 from yebblies 2012-07-10 14:02:54 EST --- (In reply to comment #79) > (In reply to comment #78) > But it does seem to be down to two problems with D's design: > - structs aren't guaranteed to be safe to just bit-copy (this problem was > introduced in D2) > - we have variadics that are really just C's variadics with typeinfo added > We also have C's variadics. > Something else I should've realised earlier: Why do D class methods need to be > directly callable from C? (How does C code hold a reference to a D object, > anyway?) Indeed, is even C++ designed to accommodate this? COM classes defined in D are callable from C (and you could define other classes the same way). -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #81 from Stewart Gordon 2012-07-10 05:05:48 PDT --- (In reply to comment #80) > (In reply to comment #79) >> - we have variadics that are really just C's variadics with >> typeinfo added > > We also have C's variadics. But no use case I can see for using a C-style variadic for a D class method. >> Something else I should've realised earlier: Why do D class methods >> need to be directly callable from C? (How does C code hold a >> reference to a D object, anyway?) Indeed, is even C++ designed to >> accommodate this? > > COM classes defined in D are callable from C (and you could define > other classes the same way). But do any COM interfaces define C-style variadic methods? Do we need to be open to this possibility, or are we wasting our time by worrying about it? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #82 from yebblies 2012-07-10 22:50:07 EST --- (In reply to comment #81) > (In reply to comment #80) > > (In reply to comment #79) > >> - we have variadics that are really just C's variadics with > >> typeinfo added > > > > We also have C's variadics. > > But no use case I can see for using a C-style variadic for a D class method. > I dunno, maybe you want to pass the args on to vprintf or something... Does it really matter? > >> Something else I should've realised earlier: Why do D class methods > >> need to be directly callable from C? (How does C code hold a > >> reference to a D object, anyway?) Indeed, is even C++ designed to > >> accommodate this? > > > > COM classes defined in D are callable from C (and you could define > > other classes the same way). > > But do any COM interfaces define C-style variadic methods? Do we need to be > open to this possibility, or are we wasting our time by worrying about it? COM does not use the C calling convention. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #83 from Stewart Gordon 2012-07-10 15:47:32 PDT --- (In reply to comment #82) > (In reply to comment #81) >> But no use case I can see for using a C-style variadic for a D class method. > > I dunno, maybe you want to pass the args on to vprintf or something... Does > it > really matter? I'd got the impression that D-style variadics are directly compatible in that respect. But if D-style variadics were something more structured, I can see that passing them to a C variadic function would be trivial. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #84 from Andrei Alexandrescu 2012-09-05 07:24:44 PDT --- Created an attachment (id=1143) Inherited contracts -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #86 from Andrei Alexandrescu 2012-09-05 07:27:40 PDT --- Forgot to mention - I attached the relevant page from the book (Walter found it) that makes it as clear as it gets how inherited preconditions should behave. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #85 from Andrei Alexandrescu 2012-09-05 07:26:07 PDT --- I've had the opportunity to discuss the matter with Bertrand Meyer himself and with a graduate student of his. Bertrand didn't have a defined answer offhand, but opined that the static contract should be evaluated. His book says the same . Julian Tschannen (who allowed me to share his name here) wrote me the following: = 1. Eiffel ECMA standard ([1], Rule 8.23.26) says, that the contract of the dynamic type is checked, i.e. "pre_A OR ELSE pre_B" (combined precondition, [1], Rule 8.10.5). 2. The Eiffel runtime does actually that, first checks the precondition of the parent class A, and then the precondition of the subclass B. My take on the issue: Dynamically it runs of course without a problem. If you would have a static checker (e.g. the AutoProof tool that I am developing), the code would be rejected due to the static check. Since we strive to get a language that is statically checked and fully verified, it would probably make more sense to just check the precondition of the static type and not take the dynamic type into account for precondition checks, since the client code works just with the given example and is not correct for all possible arguments. Or to be more precise, you could take all the static information into account, but only the static information. It would for example be possible that the client code has some precondition that would make sure that the code is statically correct, even if the call - when looked at in isolation - is statically not correct. = So we currently do what the Eiffel standard and compiler do, but not what would probably be the most sensible thing. In my opinion we should do the right thing and check the contract statically. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #87 from deadalnix 2013-01-10 00:41:57 PST --- (In reply to comment #85) > I've had the opportunity to discuss the matter with Bertrand Meyer himself and > with a graduate student of his. Bertrand didn't have a defined answer offhand, > but opined that the static contract should be evaluated. His book says the > same > . > You are lucky. I wrote him about that and he never answered me :'( . > So we currently do what the Eiffel standard and compiler do, but not what > would > probably be the most sensible thing. In my opinion we should do the right > thing > and check the contract statically. I think that this is the sane thing to do. However, this is tricky implementationwise. Maybe we should update this bug report's tag according to what you announced here : http://forum.dlang.org/thread/kcijgh$25h6$1...@digitalmars.com -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
http://d.puremagic.com/issues/show_bug.cgi?id=6857 --- Comment #88 from Andrei Alexandrescu 2013-01-10 09:14:02 PST --- @Walter: would you preapprove this? -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email --- You are receiving this mail because: ---
[Issue 6857] Precondition contract checks should be statically bound.
https://issues.dlang.org/show_bug.cgi?id=6857 Iain Buclaw changed: What|Removed |Added Priority|P2 |P3 --
Re: [Issue 6857] Precondition contract checks should be statically bound.
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 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.
Re: [Issue 6857] Precondition contract checks should be statically bound.
Please reply on bugzilla, replying here is most likely to be overlooked.
Re: [Issue 6857] Precondition contract checks should be statically bound.
On 5/6/2012 2:19 AM, d-bugm...@puremagic.com wrote: That is not this complicated. you need a final function that check the in contract, then call another virtual function that actually execute the function body and the out contract. With such a configuration, the in contract is checked and only then the virtual dispatch is done. It's not that simple. Several considerations have to be met: 1. Because of struct construction/destruction, you really only want to construct the parameter list *once*, but you're calling two functions with the same parameter list. 2. Variadic functions mean that one function cannot forward to another one using standard functions. (Perhaps a dirty magic thunk can work.) 3. The presence or absence of contracts must not change the ABI of the function. 4. The virtual table must be unchanged. 5. It's not so practical to jump into the middle of another function - things just aren't designed that way. 6. The caller now has to be aware of contracts in the called function, this was never necessary before.
