Liskov Substitution Principle (was: Pathname)

Something weird happened to my last message while trying to send it, so 
I'm sending it again, just in case. (and changing the topic too)

---------- Forwarded message ----------
Date: Mon, 23 May 2005 22:28:14 -0400 (EDT)
From: Mathieu Bouchard <[e-mail]>
To: [e-mail]
Subject: Re: [ ruby-Patches-1939 ] Pathname, totally revamped


On Tue, 24 May 2005, Sam Roberts wrote:
> Sometimes called Liskov substitution principle.
>> never override any method in a subclass, because hey, people might not
>> expect different behavior.
> You derive to override implementation, not behaviour.

To be precise, what's normally called a "subtype" may have its apparent 
behaviour be different from its "supertype" in a few ways. Let me try to 
explain this in my own words.

The Liskov requirements (from my memory) are that IF the arguments and state 
for the execution of a method are valid (preconditions), THEN the message 
should have the expected effects and return values (postconditions). This is a 
logical implication, like this:

   Precond(method,pre_state,args) -> Postcond(method,post_state,return)

So you can do this in a subtype (relative to what it is in the supertype):

1. make the preconds looser
2. make the postconds stricter
3. make the postconds looser but only in the cases where the preconds are being 
used in a looser way.

The point is that in a subtype, satisfying the Pre->Post implies satisfying the 
Pre->Post of the supertype. The above three cases are the three ways that 
semantics can be extended without violating expectations.

So, in short, Liskov's substitution principle can be written:

   (SubPre -> SubPost) -> (SuperPre -> SuperPost)

again as a logical implication.

Does that sound accurate?

,-o--------o--------o--------o-. ,---. irc.freenode.net #dataflow |
| The Diagram is the Program tm| | ,-o-------------o--------------o-.
`-o------------o-------------o-' | | Mathieu Bouchard (Montr饌l QC) |
   | t駘駱hone:+1.514.383.3801`---' `-o-- http://artengine.ca/matju -'