Re: LSP

On Fri, 22 Feb 2008 20:15:01 -0500, Daniel T. wrote:

S Perryman <q@xxxxx> 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?

An independent, but no less important issue is substitutability within the
class. That is when you write a program in terms of any type derived from T
and wish to state its correctness without knowing S, S1, S2, ... Soo.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.