411:. Unfortunately, though, it has several issues. Firstly, in its original formulation, it is too strong: we rarely want the behavior of a subclass to be identical to that of its superclass; substituting a subclass object for a superclass object is often done with the intent to change the program's behavior, albeit, if behavioral subtyping is respected, in a way that maintains the program's desirable properties. Secondly, it makes no mention of
247:). Consider a specification for the absolute value method that specifies a precondition 0 ≤ x and a postcondition result = x. The specification that specifies a precondition "true" and a postcondition result = |x| strengthens this specification, even though the postcondition result = |x| does not strengthen (or weaken) the postcondition result = x. The necessary condition for a specification with precondition P
56:. Since, for each method of type Queue, type Stack provides a method with a matching name and signature, this check would succeed. However, clients accessing a Stack object through a reference of type Queue would, based on Queue's documentation, expect FIFO behavior but observe LIFO behavior, invalidating these clients' correctness proofs and potentially leading to incorrect behavior of the program as a whole.
423:
of type T. This is problematic for several reasons, one being that it does not support the common case where T is abstract and has no implementation. Thirdly, and most subtly, in the context of object-oriented imperative programming it is difficult to define precisely what it means to universally or
24:
is the principle that subclasses should satisfy the expectations of clients accessing subclass objects through references of superclass type, not just as regards syntactic safety (such as the absence of "method-not-found" errors) but also as regards behavioral correctness. Specifically, properties
208:, and it need only ensure the result is nonnegative as well. Two possible ways to strengthen this specification are by strengthening the postcondition to state result = |x|, i.e. the result is equal to the absolute value of x, or by weakening the precondition to "true", i.e. all values for
427:
In an interview in 2016, Liskov herself explains that what she presented in her keynote address was an "informal rule", that
Jeannette Wing later proposed that they "try to figure out precisely what this means", which led to their joint publication on behavioral subtyping, and indeed that
59:
This example violates behavioral subtyping because type Stack is not a behavioral subtype of type Queue: it is not the case that the behavior described by the documentation of type Stack (i.e. LIFO behavior) complies with the documentation of type Queue (which requires FIFO behavior).
100:. This also means that behavioral subtyping can be discussed only with respect to a particular (behavioral) specification for each type involved and that if the types involved have no well-defined behavioral specification, behavioral subtyping cannot be discussed meaningfully.
71:
element, does satisfy behavioral subtyping and allows clients to safely reason about correctness based on the presumed types of the objects they interact with. Indeed, any object that satisfies the Stack or Queue specification also satisfies the Bag specification.
87:
of type T, if it has any, is completely irrelevant to this question. Indeed, type T need not even have an implementation; it might be a purely abstract class. As another case in point, type Stack above is a behavioral subtype of type Bag even if type Bag's
108:
A type S is a behavioral subtype of a type T if each behavior allowed by the specification of S is also allowed by the specification of T. This requires, in particular, that for each method M of T, the specification of M in S is
424:
existentially quantify over objects of a given type, or to substitute one object for another. In the example above, we are not substituting a Stack object for a Bag object, we are simply using a Stack object as a Bag object.
196:
the precondition. Indeed, a method specification is stronger if it imposes more specific constraints on the outputs for inputs that were already supported, or if it requires more inputs to be supported.
52:
behavior). Suppose, now, that type Stack was declared as a subclass of type Queue. Most programming language compilers ignore documentation and perform only the checks that are necessary to preserve
44:
method to remove one. Suppose the documentation associated with these types specifies that type Stack's methods shall behave as expected for stacks (i.e. they shall exhibit
405:
378:
351:
324:
25:
that clients can prove using the specification of an object's presumed type should hold even though the object is actually a member of a subtype of that type.
212:
should be supported. Of course, we can also combine both, into a specification that states that the result should equal the absolute value of
204:, that specifies a precondition 0 ≤ x and a postcondition 0 ≤ result. This specification says the method need not support negative values for
628:
428:"technically, it's called behavioral subtyping". During the interview, she does not use substitution terminology to discuss the concepts.
295:
In an influential keynote address on data abstraction and class hierarchies at the OOPSLA 1987 programming language research conference,
49:
408:
505:
17:
299:
said the following: "What is wanted here is something like the following substitution property: If for each object
45:
33:
29:
200:
For example, consider the (very weak) specification for a method that computes the absolute value of an argument
598:
Parkinson, Matthew J.; Bierman, Gavin M. (January 2008). "Separation logic, abstraction and inheritance".
75:
It is important to stress that whether a type S is a behavioral subtype of a type T depends only on the
63:
In contrast, a program where both Stack and Queue are subclasses of a type Bag, whose specification for
192:). That is, strengthening a method specification can be done by strengthening the postcondition and by
48:
behavior), and that type Queue's methods shall behave as expected for queues (i.e. they shall exhibit
353:
of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when
580:
607:
553:
517:
461:
383:
356:
329:
302:
482:
537:
296:
407:, then S is a subtype of T." This characterization has since been widely known as the
622:
125:
117:
53:
574:
287:". Indeed, "result = |x| or false" does strengthen "result = x or x < 0".
611:
466:
449:
558:
541:
506:"Behavioral subtyping, specification inheritance, and modular reasoning"
522:
223:
Note, however, that it is possible to strengthen a specification ((P
92:
exhibits FIFO behavior: what matters is that type Bag's
255:
to be stronger than a specification with precondition P
510:
454:
386:
359:
332:
305:
96:
does not specify which element is removed by method
504:Leavens, Gary T.; Naumann, David A. (August 2015).
542:"Keynote address - data abstraction and hierarchy"
399:
372:
345:
318:
448:Liskov, Barbara; Wing, Jeannette (1994-11-01).
415:, so it invites an incorrect reading where the
132:is stronger than one given by a precondition P
499:
497:
239:)) without strengthening the postcondition (Q
8:
443:
441:
557:
521:
465:
391:
385:
364:
358:
337:
331:
310:
304:
437:
7:
409:Liskov Substitution Principle (LSP)
450:"A behavioral notion of subtyping"
116:A method specification given by a
14:
573:van Vleck, Tom (April 20, 2016).
583:from the original on 2021-12-21.
490:(PhD). University of Cambridge.
40:method to add an element and a
481:Parkinson, Matthew J. (2005).
104:Verifying behavioral subtyping
1:
576:Interview with Barbara Liskov
419:of type S is compared to the
326:of type S there is an object
28:For example, consider a type
629:Object-oriented programming
18:object-oriented programming
645:
67:is merely that it removes
484:Local reasoning for Java
612:10.1145/1328897.1328451
401:
374:
347:
320:
467:10.1145/197320.197383
402:
400:{\displaystyle o_{2}}
375:
373:{\displaystyle o_{1}}
348:
346:{\displaystyle o_{2}}
321:
319:{\displaystyle o_{1}}
279:" is stronger than "Q
136:and a postcondition Q
384:
357:
330:
303:
36:, which both have a
22:behavioral subtyping
600:ACM SIGPLAN Notices
559:10.1145/62139.62141
546:ACM SIGPLAN Notices
380:is substituted for
259:and postcondition Q
251:and postcondition Q
216:, for any value of
113:than the one in T.
397:
370:
343:
316:
291:"Substitutability"
180:is stronger than Q
83:) of type T; the
636:
615:
585:
584:
570:
564:
563:
561:
534:
528:
527:
525:
501:
492:
491:
489:
478:
472:
471:
469:
460:(6): 1811–1841.
445:
406:
404:
403:
398:
396:
395:
379:
377:
376:
371:
369:
368:
352:
350:
349:
344:
342:
341:
325:
323:
322:
317:
315:
314:
267:is weaker than P
644:
643:
639:
638:
637:
635:
634:
633:
619:
618:
597:
594:
589:
588:
572:
571:
567:
536:
535:
531:
523:10.1145/2766446
503:
502:
495:
487:
480:
479:
475:
447:
446:
439:
434:
387:
382:
381:
360:
355:
354:
333:
328:
327:
306:
301:
300:
293:
286:
282:
278:
274:
270:
266:
262:
258:
254:
250:
246:
242:
238:
234:
230:
226:
191:
187:
183:
179:
175:
171:
167:
159:
155:
151:
147:
143:
139:
135:
131:
123:
106:
12:
11:
5:
642:
640:
632:
631:
621:
620:
617:
616:
593:
590:
587:
586:
565:
529:
493:
473:
436:
435:
433:
430:
421:implementation
417:implementation
413:specifications
394:
390:
367:
363:
340:
336:
313:
309:
297:Barbara Liskov
292:
289:
284:
280:
276:
272:
268:
264:
260:
256:
252:
248:
244:
240:
236:
232:
228:
224:
189:
185:
181:
177:
173:
169:
165:
157:
153:
149:
145:
141:
137:
133:
129:
121:
105:
102:
90:implementation
85:implementation
13:
10:
9:
6:
4:
3:
2:
641:
630:
627:
626:
624:
613:
609:
605:
601:
596:
595:
591:
582:
578:
577:
569:
566:
560:
555:
551:
547:
543:
539:
533:
530:
524:
519:
515:
511:
507:
500:
498:
494:
486:
485:
477:
474:
468:
463:
459:
455:
451:
444:
442:
438:
431:
429:
425:
422:
418:
414:
410:
392:
388:
365:
361:
338:
334:
311:
307:
298:
290:
288:
221:
219:
215:
211:
207:
203:
198:
195:
163:
140:(formally: (P
127:
126:postcondition
119:
114:
112:
103:
101:
99:
95:
94:specification
91:
86:
82:
81:documentation
78:
77:specification
73:
70:
66:
61:
57:
55:
51:
47:
43:
39:
35:
31:
26:
23:
19:
606:(1): 75–86.
603:
599:
575:
568:
552:(5): 17–34.
549:
545:
540:(May 1988).
532:
513:
509:
483:
476:
457:
453:
426:
420:
416:
412:
294:
222:
217:
213:
209:
205:
201:
199:
193:
161:
118:precondition
115:
110:
107:
97:
93:
89:
84:
80:
76:
74:
68:
64:
62:
58:
41:
37:
27:
21:
15:
54:type safety
32:and a type
592:References
538:Liskov, B.
79:(i.e. the
263:is that P
194:weakening
188:implies Q
172:implies P
623:Category
581:Archived
283:or not P
275:or not P
111:stronger
579:. ACM.
184:(i.e. Q
176:) and Q
168:(i.e. P
156:)) if P
271:and "Q
231:) ⇒ (P
164:than P
162:weaker
148:) ⇒ (P
124:and a
516:(4).
488:(PDF)
432:Notes
34:Queue
30:Stack
69:some
50:FIFO
46:LIFO
608:doi
554:doi
518:doi
462:doi
243:⇏ Q
235:, Q
227:, Q
160:is
152:, Q
144:, Q
98:get
65:get
42:get
38:put
16:In
625::
604:43
602:.
550:23
548:.
544:.
514:37
512:.
508:.
496:^
458:16
456:.
452:.
440:^
220:.
20:,
614:.
610::
562:.
556::
526:.
520::
470:.
464::
393:2
389:o
366:1
362:o
339:2
335:o
312:1
308:o
285:t
281:t
277:s
273:s
269:t
265:s
261:t
257:t
253:s
249:s
245:t
241:s
237:t
233:t
229:s
225:s
218:x
214:x
210:x
206:x
202:x
190:t
186:s
182:t
178:s
174:s
170:t
166:t
158:s
154:t
150:t
146:s
142:s
138:t
134:t
130:s
128:Q
122:s
120:P
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.