Liskov substitution principle | EPFL Graph Search

Are you an EPFL student looking for a semester project?

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

The Liskov substitution principle (LSP) is a particular definition of a subtyping relation, called strong behavioral subtyping, that was initially introduced by Barbara Liskov in a 1987 conference keynote address titled Data abstraction and hierarchy. It is based on the concept of "substitutability" a principle in object-oriented programming stating that an object (such as a class) may be replaced by a sub-object (such as a class that extends the first class) without breaking the program. It is a semantic rather than merely syntactic relation, because it intends to guarantee semantic interoperability of types in a hierarchy, object types in particular. Barbara Liskov and Jeannette Wing described the principle succinctly in a 1994 paper as follows: 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. Symbolically: That is, if S subtypes T, what holds for T-objects holds for S-objects. In the same paper, Liskov and Wing detailed their notion of behavioral subtyping in an extension of Hoare logic, which bears a certain resemblance to Bertrand Meyer's design by contract in that it considers the interaction of subtyping with preconditions, postconditions and invariants. Liskov's notion of a behavioural subtype defines a notion of substitutability for objects; that is, if S is a subtype of T, then objects of type T in a program may be replaced with objects of type S without altering any of the desirable properties of that program (e.g. correctness). Behavioural subtyping is a stronger notion than typical subtyping of functions defined in type theory, which relies only on the contravariance of parameter types and covariance of the return type. Behavioural subtyping is undecidable in general: if q is the property "method for x always terminates", then it is impossible for a program (e.g. a compiler) to verify that it holds true for some subtype S of T, even if q does hold for T.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (1)

Related concepts (14)

Related courses (7)

Related lectures (50)

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

MATH-458: Programming concepts in scientific computing

The aim of this course is to provide the background in scientific computing. The class includes a brief introduction to basic programming in c++, it then focus on object oriented programming and c++ s

CS-450: Advanced algorithms

A first graduate course in algorithms, this course assumes minimal background, but moves rapidly. The objective is to learn the main techniques of algorithm analysis and design, while building a reper

Object-oriented programming

Object-Oriented Programming (OOP) is a programming paradigm based on the concept of "objects", which can contain data and code. The data is in the form of fields (often known as attributes or properties), and the code is in the form of procedures (often known as methods). A common feature of objects is that procedures (or methods) are attached to them and can access and modify the object's data fields. In this brand of OOP, there is usually a special name such as or used to refer to the current object.

Liskov substitution principle

Inheritance (object-oriented programming)

In object-oriented programming, inheritance is the mechanism of basing an object or class upon another object (prototype-based inheritance) or class (class-based inheritance), retaining similar implementation. Also defined as deriving new classes (sub classes) from existing ones such as super class or base class and then forming them into a hierarchy of classes. In most class-based object-oriented languages like C++, an object created through inheritance, a "child object", acquires all the properties and behaviors of the "parent object", with the exception of: constructors, destructors, overloaded operators and friend functions of the base class.

Flexible subtyping relations for component-oriented formalisms and their verification

David Huerzeler

In this thesis we address the problem of safe substitutability in mobile component-oriented formalisms. We try to give a solution for different definitions of "safe" through a new notion of subtyping

EPFL2004

Explores the challenges of null references in programming languages and proposes solutions to mitigate their drawbacks while ensuring compatibility with existing codebases.

Covers the concept of unfolding recursive functions using the Stainless tool.

Introduces the Stainless verification tool with examples of verifying commutativity properties and arithmetic operations.