Re: LSP

"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.

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.

Or maybe you have a method to determine which code is random?

Yes, of course, code who's behavior is undefined. It is quite
easy to tell when the behavior of a function is undefined...

That's interesting. Are you saying that an implementation of a
function does not define its behavior?

Yes, that is exactly what I am saying. After all, the first question
that can be asked of any implementation is, "is that implementation
correct?" You can't know if the implementation is correct unless the
behavior of the function has been defined *independent of the
implementation*.

As a simple example. If the two types that you have implemented are
defined as follows (using the specification language defined in Liskov's
paper...)

T = type
for all t: T

invariant true
constraint true

One = proc ( x : P )
requires false

end T

S = type
for all s: S

invariant true
constraint true

One = proc ( x : P )
requires false

end S

Then both implementations are correct (regardless what HALT does) and
the types are substitutable for each-other. QED.
.

Relevant Pages

  • Re: LSP
    ... you have to properly specify the types. ... define subtyping in terms of some formal meta language of contracts ... not in terms of substitutability. ...
    (comp.object)
  • Re: LSP
    ... you have to properly specify the types. ... but you were unable to prove substitutability. ... Not "for whatever reason", for the reason that you have not specified ...
    (comp.object)
  • Re: LSP
    ... you have to properly specify the types. ... but you were unable to prove substitutability. ... Not "for whatever reason", for the reason that you have not specified ...
    (comp.object)
  • Re: LSP
    ... you have to properly specify the types. ... some random code, not type specifications. ... but you were unable to prove substitutability. ...
    (comp.object)