Re: LSP

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.

Obviously not true, because of undecidability.

If I construct something like the Halting problem (which is what I expect
Dmitry Kazakov meant when replying to you) in Liskov/Wing notions
(invariant/pre/post conditions etc) , the subtype predicate cannot give
a value of true/false by definition.


Regards,
Steven Perryman
.

Relevant Pages