Re: LSP

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

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... No definition has
been written for it. QED indeed.
.

Relevant Pages

  • 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. ... substitutability. ...
    (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)
  • 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)