A semantic approach to defining subtyping in ObjectOrientedDesign and ObjectOrientedProgramming (I would say design first). 

	 :	... The objects of subtype ought to behave the same as those of the supertype as far as anyone or any program using the supertype objects can tell.

The problem is of course what we do understand by ''behave the same''. First of all it should be obvious that the usage of objects of subtype in lieu of objects of the supertypes should not generate '''type errors''' (statically or dynamically for dynamically typed languages). Therefore a subtype has to provide the expected methods for the compatible signatures  (what exactly are the expected methods and compatible signatures, it's a whole new discussion, but the generally favored approach is to use covariance for return and exception types and contravariance for argument types).

However this Liskov and Wing argues that merely passing a type check is not enough. For example we can expect that Stack and Queue might have perfectly compatible method signatures  : void add(Object), Object get(), int size() ... etc. So either one can be a subtype of the other as far as a type checker is concerned but logically and semantically they are not.

They add the following condition:

	 :	''Subtype Requirement'': Let ''phi''(x) be a property provable about objects x of type '''T'''. Then ''phi''(y) should be true for objects y of type '''S''', where '''S''' is a subtype of '''T'''. 

	 :	A type's specification determines what properties we can prove about objects.
 
See: http://www-2.cs.cmu.edu/afs/cs/project/calder/www/fmdp.html 

Barbara Liskov, Jeanette Wing: "Behavioural Subtyping Using Invariants and Constraints ", July 1999, CMU-CS-99-156 MIT Lab

An older formulation is
	 :	What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for '''all''' programs P defined in terms of T, the behavior of P is '''unchanged''' when o1 is substituted for o2 then S is a subtype of T." - BarbaraLiskov, Data Abstraction and Hierarchy, ''SIGPLAN Notices'', 23,5 (May, 1988).

----

'''Arguments against'''
	* The math is unsound.
		* It's a definition.  Definitions cannot be unsound (at least not in that sense).  It can be shown to be unfit for some purpose.  In this case, it would be a major blow if every subtype (S) of a type (T) was actually of that type.  I.e. if T :> S implies that T = S.
		* See SuperCommutativity for another example of how a definition can't be unsound.  The intent was to create an unsound definition, and ended with another name for "=".
	* The following show that the only subtype of T is T.
 class P ( ...'
  public boolean broken( T theArg ) {
  return (theArg.getClass().getName().equals("T"));
and

 program(t){
	print t.type.name
 }
.
		*No they don't.  The behavior for these methods aren't specified.  For the definition of behavior used in LiskovWingSubtyping, a type that doesn't specify the behavior of a method is considered to match any object that supports that method.  This means that a potential subtype (of T) S could return "S" from t.type.name and still be considered a subtype.

----

'''Examples'''

A stack is not a subtype of a queue, or vice versa.  But they are both subtypes of a collection, defined in this manner:
 class Collection {
	// Returns and removes an object previously put in the collection.
	public Object get();

	// Inserts an object into the collection.
	public void put(Object);
 }

 class Queue {
	head = 0;
	tail = 0;
	array = {};

	public Object get(){
		if (head==tail) throw Error();
		return array[head++];
	}

	public void put(Object){
		array[tail++]=Object;
	}
 }

 class Stack {
	integer index = 0;
	Object[] array = {};

	public Object get(){
		if (index==0) throw Error()
		return array[--index];
	}

	public void put(Object){
		return array[index++];
	}
 }
There is no valid assumption that one can make from the interface of Collection that will ever be violated by Stack or Queue.

This approach can explain the issue with Alastair's counter-example:
 class Collection {
	// Returns and removes an object previously put in the collection.
	public Object get();

	// Inserts an object into the collection.
	public void put(Object);

	// Returns a Strng containing the name of the implementation of this class.
	public Class getClass();
 }

 class Queue {
	head = 0;
	tail = 0;
	array = {};

	public Object get(){
		if (head==tail) throw Error();
		return array[head++];
	}

	public void put(Object){
		array[tail++]=Object;
	}

	public String getClass(){
		return "Queue";
	}
 }

 class Stack {
	integer index = 0;
	Object[] array = {};

	public Object get(){
		if (index==0) throw Error()
		return array[--index];
	}

	public void put(Object){
		return array[index++];
	}

	public String getClass(){
		return "Stack";
	}
 }
The fact the their behaviour is the same under that interface is trivially true;  that the information made available due to the result of the 'getClass()' function is part of the interface is trivially false.

The trick is that in this context, the behaviour of getClass() is specified to be an open set, whereas get() and put() are a closed set.  The behaviour of get() and put() is completely determined by the closed set of 'what have we put in so far'.  Stack and Queue would therefore not be subtypes of Collection if they violated this, either by returning an object from get() that had not been added by means of put().  getClass(), on the other hand is an open set.  Therefore, any program making valid use of the interface must be prepared to accept any output which satisfies the predicate of that open set, namely, that there is a definition of a class, whose name is represented by the returned String.  And here is the important part:  any program that breaks given the output of any subclass of collection is making invalid use of that interface.  More formally, any program which uses the output of getClass() must either map it to a closed set, or include an open set as part of its interface.  Note that the opposite is not true:  a closed set can never possibly generate an open set;  to do otherwise would invalidate the HaltingProblem.

Given this, we can come up with a simple definition of behaviour which has the property described above:  the behaviour of a type is the [set of [mapping of a open or closed set to a function names]].

"If for each object o1 of type S there is an object o2 of type T such that for '''all''' programs P defined in terms of T, the behavior of P is '''unchanged''' when o1 is substituted for o2 then S is a subtype of T."

For any program defined in terms of Collection's, the behaviour (as defined above) is unchanged if used with Queue or Stack.  If it makes use of getClass(), and makes a decision on the basis of that output, then it's behaviour can already be described as returning an open or closed set.
 String closedSetBehaviour(Collection){
	string = Collection.getClass();
	if (string=="Queue")
		return true;
	else
		return false;
 }

 String openSetBehaviour(Collection){
	string = Collection.getClass();
	if (string=="ClearableQueue")
		return ((ClearableQueue) Collection).clearAll();
	else
		return false;
 }
Remember, that this is defined in terms of Collection, and therefore the result of any cast-like activity is an open set.  There behaviour is therefore not changed in either example:  the first will always return a known closed set, the other an open set.  

In short, we're talking about 'behaviour' as in the behaviour of functions of the form "f(x) = a / bx", as opposed to the behaviour of the function in which "f(x) = 6 / 3x == 1 where x=2".

Another phrasing would be:  Behaviour is the set of things that a subtype ''could'' do, not the set of things that it ''will'' do.

--WilliamUnderwood

P.S., for the TuringChallenged, I define an open set loosly as a set that could always fill up the memory of any available computer, wheras a closed set can always be completely enumerated on a sufficiently powerful real computer.


----

Let's be very very clear about what this page is discussing, since people slide around very quickly. 

''Alistair. let's be very clear that this page '''shall not be''' about Alistair's misunderstandings and personal itches. We have LiskovSubstitutionPrinciple for that. This page is about LiskovWingSubtyping. The paper I quoted above contains the proper definition of a mathematically sound approach to subtyping, which also has practical value and will have even more when we get rid of SoftwareEngineeringVsComputerScience attitude.''

''You came with two programs which don't prove anything except that you didn't understand the content of the papers, and you can't get beyond some personal animosity or whatever is you have (and traces of that can be found in the original LiskovSubstitutionPrinciple). ''

''I'm tired to repeat the argument over and over again, but the '''behavior''' in their research is a very strict mathematical concept and it does not mean that your little program should always return the same result, so you don't prove anything, really. --CostinCozianu''

Hi, Costin - All you have to do is write down a definition of subtyping that works. That's all you have to do. When you do that, we can get the discussion back on track. --AlistairCockburn

''I don't have to do anything like that, this is what the paper cited above is about, and the essence of it is sketched on this page for whoever bothers to actually read. -CostinCozianu''

-----
There is a declaration attached to a research goal. The declaration is is:

	 :	"What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for '''all''' programs P defined in terms of T, the behavior of P is '''unchanged''' when o1 is substituted for o2 then S is a subtype of T." - 1. BarbaraLiskov,  Data Abstraction and Hierarchy,  ''SIGPLAN Notices'', 23,5 (May, 1988).

The research goal is: 

	 :	'''Behavioural Subtyping''' "A small number of research groups around the world are working on the concept of behavioural subtyping. In this approach, subtyping is based not only on type names and/or signatures, but also on a a description of the type's behaviour." (from http://www.dstc.edu.au/AU/research_news/odp/typemgmt/related_work/behav_subtype.html)

Please note the operative words, "all programs" and "unchanged". These people are talking about mathematics, not programming heuristics. 

There are two very distinct questions for this page.
	* Whether the math is sound. 
	* Whether the heuristic is useful, regardless of whether the math is sound.
-----
AlistairCockburn posits (1) that the math is unsound, while (2) the heuristic is still useful on many occasions. Alistair's argument is put forth at http://members.aol.com/humansandt/papers/subtyping.htm. 

Disproving the math is a simple matter: produce a counterexample. If there is so much as one single computer program for which Liskov's substitution property does not hold, then '''mathematically''' speaking, her declaration is not valid and the research projects to define her property are futile.

AlistairCockburn and SunirShah each generated such a program. The first is 

 class P ( ...'
  public boolean broken( T theArg ) {
  return (theArg.getClass().getName().equals("T"));

and the second is

 program(t){
	print t.type.name
 }

The challenge for anyone who wishes to defend the declaration is to present a mathematical definition of subtyping that permits subtypes of T to be substituted for T in the above two programs without altering their behavior.  Alistair believes this is not only impossible, it is trivially easy to see that it is impossible.

''Their "behavior" is actually unaltered. The "behaviour is not changed" does not mean the program allways return a constant. It's very basic. The behavior of a program is a relation between its inputs, outputs, and possibly the context of execution. ''

''If I write F(x)= x+1 the behavior of F is the predicate:''
 OUTPUT = INPUT + 1 
''which holds true for every x that doesn't generate a type checking error (of course we can't substitute x with a string). It doesn't have to be the predicate "OUTPUT = constant". This is the very basic logical flaw in asserting that the above two programs disproves whatever. By the way, you can't have a counterexample to a definition. --Costin''
----

This is an attempt to refactor the confusing discussion from LiskovSubstitutionPrinciple. As a matter of fact I have strong reasons to believe that Barabara Liskov never asserted a LiskovSubstitutionPrinciple. 

The discussion on that page got confused over several issues, starting with the definition of ''program behavior'', using a very old definition, and mixing a lot of issues that are not related to LiskovWingSubtyping.  --CostinCozianu
------
There are several things to pay attention for:

	*Even if OO programmers are used to inheritance and/or interface implementation automatically providing subtyping as far as languages such as C++,Java,Smalltak are concerned, this is not what LWS discusses. We need to have something more than that in order to design and construct useful and correct OO programs and especially OO frameworks. Several researchers argued that the confusion between inheritance and subtyping is one of the biggest hurdles we have to overcome with our current OO technologies.
	*We need to extend the understanding of type from merely the synctactic declaration of a class/interface in C++/Java, with a specification of the properties (axioms) of that type. Clients of the type and its subtypes will have then an instrument to reason about the correctness of their program. Ideally this should be done in a specification language, but current OO technologies can't do that (Eiffel comes closest to this ideal). We might settle for informal methods like the documentation of the class (JavaDoc/DoxyGen), unit tests, etc... See the quoted paper for a relevant example of a formal specification language used to fully specify the definition of a type.
-----
The decision whether a type is a behavioural subtype of another is a logical design choice, it is more than having a class inherit from another or an interface inherit from another, or having a class implement an interface, or in dinamically type checked languages having a class implement an expected set of methods.

Clearly that is not enough, it is only a mechanical assurance that we will not have type errors. However we are more interested of the correctness of the program results. In this LiskovWingSubtyping is a very sound design principle that should be applied.
-----
AlistairCockburn argued that such a definition of subtyping is either broken  or not useful for practical purposes, therefore even if it works in theory it shouldn't be used as a cornerstone design principle. 

(Correction, please read my writing (the online version of "read my lips"). The math is unsound, the heuristic is useful under several circumstances nonetheless. --AlistairCockburn)

See:
 http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/www/subtype-tr.html for 
 http://www.objectmentor.com/publications/lsp.pdf. 

He addresses two practical things that in his opinion break the LSP: mutability and reflection.

As a matter of fact Liskov and Wing do address mutability in the above paper, it is true that they don't address reflection. However, reflection cannot break the LiskovWingSubtyping, because LWS is a logical design choice. I addressed that in the discussion of LiskovSubstitutionPrinciple.

It is arguable that LSW might be too tough of a restriction in order to allow practical usage, i.e  we'll rarely meet a type that is a LWS subtype of another in practical design, and we might want to use a lesser relation: ''is kind-of'' between types, that would allow a more flexible framework for OO designers and programmers to work with.

However, the proponents of this approach have yet to come up with practical examples where LWS is too strict, and have yet to construct and logically justify an alternative. 

----
As I see it, the issue is not if LWS is to restrictive for practical use. It is whether the cost of violating it is worth the additonal expressive power. Subclassing can be used to implement subtyping ( Data Abstraction and Heirarchy section 3.3) but not all subclasses are or should be subtypes. The purpose of the research is type safety ( A behavioral notion of Subtyping). In most OOP languages the type Hierarchy and the class Hierarcy are the same. Liskov et el are suggesting that this is an error and has consequeces for language design and good practice. It is well known that subclass carries  the  burden of  high coupling. The sugestion is that with subtypes as per LWS, the price is worth it and the type system can be used to prevent the brittle base class problem, but only if , as has been descriped here so well, the behavior can be exaustively and formally descriped.

LSP/LWS is defining  what subtyping should be if you wish to it be type safe. It is a formal notion that says 'if your language system follows these rules then you can use the type system to avoid behavior related bugs in the face of implementation changes to your base class'. It also means that if your language system does not enforce these rules then you, as a programer, will need to do some thinking on your own or live with the consequences. What we call subclassing is not subtyping as defined by LSP; but the type system acts as if it can reason in a type safe manner and the result is that the type system misses bugs that a properly defined and implemented type system could catch. This is the point of the research project as I understand it.

MarcGrundfest 
-----


----
Stupid question for those who want to disprove the LSP or LWS with a single program: doesn't that single program only prove that the programming language it is written in is not LSP conforming? Can someone prove that no programming language exists where LSP can hold for any two types? --AndrewQueisser

Sorry, I didn't invent LSP or the claim. Please note that Liskov wants to search for a binary property '<' such that S < T and S can be substituted for '''all''' programs. I didn't make that up, she did. (p.s. See SuperCommutativity for a simpler arithmetic analog of this same foolishness) --AlistairCockburn

Alistair, you're a very smart guy, do you really believe what you wrote? It's been a while since I read the original LSP paper but I'm pretty sure that Liskov is not searching for that property in '''all''' languages/'''all''' environments. I do agree that LSP is in practice of dubious value but, remember, Liskov is a scientist, not an engineer. --AndrewQueisser

''If you look at the top of the page you will see that the original quote does indeed request a property present in '''all''' programs that are expressed in terms of the type T.''

(Right. If anyone in the type theory / subtyping community would publish a recant of the original goal, or publicize a weaker goal, I'd be quite happy. But as recently as 1999 JeannetteWing published yet another paper aiming at the same goal. --AlistairCockburn)

The "'''all''' languages" part is irrelevant. If I define my [abstract] type as something that doesn't know about the ''type.name'' property, then speaking about this property for some language-defined type that must contain such a property is '''not speaking in terms of my type''', and thus cannot be considered as the basis for rejection of LSP for my type. --NikitaBelenki . . . ''(Right you are, Nikita, I removed the "all languages" phrase. --Alistair)''

Thanks, Nikita, that's a good point; I hadn't played with it before. There are two ways out, both of which eliminate LWS/LSP from use. 

The first is to include type.name as a valid operation, since it can certainly be used as an operation in some applications (omitting it from the type signature is a serious omission, i.e., mistake)... In this case, trivially, no type S ever is a subtype of any other type T, and LWS/LSP vanish in a twinkling.  

The other way out is to say that type.name is not and can not be considered as part of the type signature at all, since it is a meta-construct provided by the environment... In this case, LWS/LSP simply becomes inapplicable when working in reflective environments such as  Java/Ruby/Smalltalk/C++/etc. --AlistairCockburn

The LWS is surely inapplicable for a description of a legacy type system of <put your favorite programming language here>. As well as this type system is inapplicable for a description of how the pipeline of <put your favorite processor core here> works. But they aren't supposed to! It is a pity that processor designers generally cannot implement ''language-defined type systems'' in silicon, and that language designers generally cannot implement ''behavioral type systems'' in languages, but how can you say that this alone eliminates these type systems from use? --nb

-----
After this kind of personal attacks on two people who are not on this forum, I can't help but let you know that at best you sufferred from an attack of infatuation and egocentrism that totally blinded you, and at worst you're incapable of reading a scientific paper and having an argument in good faith. 

The reality is that all your articles on the subject are not only flawed in their intention, but irrelevant since they tackle a mathematical subject without the least mathematical rigour, and pretend they prove something. Maybe you hope that the reader will fill in the missing definitions and proofs and do the work you couldn't do yourself, and maybe they will come to your conclusion. This is highly unlikely, but as long as you've chosen to skip the mathematical details you should cut down on your arrogance with which you throw assertions around.

Precisely you failed to define mathematically what you understand by behavior, yet you claim that your little programs '''change their behavior'''. Even if you'll finally be able to grasp what behavior stands for in behavioral subtyping, you will not be able to disprove what is essentially a definition of a proposed concept. The LWS is not about a theorem it's about a concept of subtyping. That the definition is sound is absoulutely obvious, at the very limit we can have the trivial system where subtype-of == is-identical-with, thus the definition is non-contradictory. The fact that we can have subtyping relations beyond the trivial one is proven with concrete examples in the papers we talk about. So the mathematical unsoundness is out of the question, like it or not. 

The best you can hope for is to prove that the concept is neither useful nor relevant, or that other concepts are more desirable to operate with, because LWS might fail to contain certain situations that intuitively, or for other considerations, should be treated as subtyping.

And here you come up with the little program that uses reflection 
 F(x:X) = ( x.type.name == "X" ) 
, which, you imply, should return true. But for many people other than you, it's obvious that's not necessarily true, not in Java, not in Smalltalk, not in any hypothetical language that would actually enforce LWS. That doesn't mean that the behavior of F has changed, because the behavior of F is what we can prove of F (and of course we can't prove that it should return true). Even from a heuristic point of view, claiming that F should always return true serves no purpose whatsoever.

So we have to either say that LWS is an unuseful concept because it doesn't allow your little program to always return true, or we have to live with the fact that F will not always return true in a system adhering to LWS. 

Yes, F doesn't always return true, we can't therefore claim that the behavior of F is to always return true in the hypothetical system supporting LWS. Only if we could justifiably claim (or better, actually prove ) that F should return true, then we could assert that the behavior has changed. 

So what's the big deal about that, Alistair ?  F doesn't always return true, just get over it. Do you have a valid claim why is it so important that F should always return true ? No, you don't. You didn't in your paper and you didn't some time ago when we had the same discussion on the LiskovSubstitutionPrinciple. If you came with something like ''If we hold LWS, than Pythagora's theorem is no longer a theorem'', then you'd have had a point. But instead you come up with a stupid little program that will not always return true, and in fact, it shouldn't. And to supplement it, you derail the discussion with politics and personal itches. 

At least did you hask the opinion of the persons you talk about so unpleasantly? Maybe they have more patience than I did to explain the obvious to you. But I wouldn't blame them if they didn't. --CostinCozianu

In fact, I did ask JeannetteWing, in 1999 before submitting my paper. She wrote back: 

''"Dear Alistair, I read what you wrote. There's nothing inherently wrong with what you're saying. It's just a matter of how useful or convenient it is to have a notion of substitutability/subtyping when one must always consider the additional argument (context)."''

Please read her words, - there's nothing inherently wrong with what I'm saying - (she chooses to pursue her research anyway). And thank you very much, you now seem to accept it, too, judging from your latest append. -- AlistairCockburn

I think that only if you twist her words, you can draw the conclusion that she agreed to all your claims that LSP is broken, or mathematically unsound and others like that. If you twist what I said maybe you can say the same about me.

The fact that your proposed subtyping relation (with the addition of context) might be a valid one, albeit not necessarily useful, does not invalidate LWS. This is also what you didn't get it right in your paper, that various researchers don't necessarily contradict each other with their proposed concept of subtyping, they just have alternative approaches, it's exactly the same as the fact that no 2 OO languages can agree on what is the a class. 

And the same with the fact that we have euclidean geometries and non-euclidean geometries. If I want to calculate the height of a building using optical instruments and for many other practical and purposeful task, I'll have the euclidean geometry anytime. Likewise if I have to choose between a system with LWS and a system like yours with subtyping depending on context, you can guess what I'd choose. You fail to produce convincing evidence where subtyping is not possible under LWS definition but is desirable under yours. 

To do so you might want to start your own constructive argument (how about AlistairSubtyping page), and give up on bashing LWS with ridiculous claims, like "is mathematically unsound", "is broken", etc. The fact that she chose to pursue her research anyways says that she didn't see much value in your proposal, and it's your responsibility to promote your ideas, not hers. But you don't need to mislead people with bashing their work in order to do that. --CostinCozianu

I think at this point, Costin, I'm willing to let our disagreement stand [AgreeToDisagree]. --AlistairCockburn
----

In case this clarifies anything:  

For class P, such that
 class P ( ...'
	public boolean broken( T theArg ) {
		return (theArg.getClass().getName().equals("T"));
	}
 }
The behaviour of broken(T) is that it will return true if the name of the class of the parameter is T.  Renaming to better describe the behaviour therefore:
 class P ( ...'
	public boolean isClassNamedT( T theArg ) {
		return (theArg.getClass().getName().equals("T"));
	}
 }

--WilliamUnderwood