Re: LSP
- From: "Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx>
- Date: Sat, 23 Feb 2008 22:26:59 +0100
On Sat, 23 Feb 2008 14:18:54 -0500, Daniel T. wrote:
"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> wrote:
Daniel T. wrote:
"Dmitry A. Kazakov" wrote:
Daniel T. wrote:
"Dmitry A. Kazakov" wrote:
Daniel T. wrote:
S Perryman wrote:
Completeness and decidability are the ultimate arbiters
of proof systems.
Given any two types, it is easy to discern wither one is
substitutable for the other and once a type is defined,
the properties that determine if it is substitutable for
another type are immutable, so I see no problem.
The problem is that your statement is wrong:
class T
{
public :
int One (P& x) { return 1; }
};
class S
{
public :
int One (P& x) { return HALT (x); }
};
Is S substitutable for T?
First, you have to properly specify the types. All you have
above is some random code, not type specifications. Specify
the types according their Liskov contracts and it will be
easy to tell.
for whatever reason, but you were unable to prove
substitutability.
Not "for whatever reason", for the reason that you have not
specified the behavior of the types. All you did was throw some
code on the screen.
But that is all what need to be shown. If you cannot derive
behavior from a full implementation of the types, then you cannot
decide whether these types are substitutable.
What you have shown is the least of what needs to be known. Behavior can
be derived from a full implementation (you didn't actually provide a
full implementation though,) but *correct* behavior cannot.
The *correct* behavior is what needs to be known.
I don't see difference. Consider behavior correct - let we have S and T
(implementations of). You have a problem with:
S, T |= S is a subtype of T
But what about:
Correct(S), Correct(T), S, T |= S is a subtype of T
where Correct(x)=true when x is correct. I gave you what you missed but you
still cannot prove the right side.
First you claim that you can, and then immediately start asking me
to do it for you!
No, I'm asking you to define the behavior of the two types in question:
preconditions, post-conditions, invariants and constraints. You have yet
to do that.
Ah, no, you should have said that. This is a quite different case. If you
define subtyping in terms of some formal meta language of contracts
(pre-/post conditions etc), then we are in agreement with regard of the
notion of subtyping. I didn't know that you meant that, because of course
Contract(T) is not T
Yes, contracts can be sufficiently weakened in order to make subtyping
decidable. But then this "subtyping" will be defined in terms of contracts,
not in terms of substitutability.
[...]
P.S. I disagree with your use of the word "behavior." I would say
"contracted behavior" instead.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.
- References:
- Prev by Date: Re: LSP Was: Mixing OO and DB
- Next by Date: Re: LSP
- Previous by thread: Re: LSP
- Next by thread: Re: LSP
- Index(es):
Relevant Pages
|
