Liskov Wing Subtyping

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

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

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


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.


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:


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


EditText of this page (last edited August 9, 2010) or FindPage with title or text search