可替换性是面向对象编程中的一个原则，指的是在计算机程序中，如果S是T的一个子类型，那么T类型的对象可以被S类型的对象替换（即，T类型的对象可以被S子类型的任何对象替换），而不改变程序的任何原定的属性（正确性、执行的任务等）。更正式地说，李斯科夫替代原则（LSP）是一种亚类型关系的特殊定义，称为（强）行为亚类型，最初是由芭芭拉·李斯科（Barbara Liskov）夫在1987年题为数据抽象和层次结构的会议主旨演讲中提出的。这是一种语义关系，而不仅仅是句法关系，因为它旨在保证层次结构中类型的语义互操作性，尤其是对象类型。芭芭拉·李斯科夫和珍妮特·荣格（Jeannette Wing）在1994年的一篇论文中简洁地描述了这一原则如下：
子类型要求：使 为
T 类型对象 的可证明属性 . 则 对于
S 类型对象 应该为真，其中
S 是
T 的子类型。
在同一篇论文中，李斯科夫和荣格在霍尔逻辑的扩展中详述了他们的行为亚类型概念，这与伯特兰·迈耶的契约设计有一定的相似性，因为它考虑了亚类型与前置条件、后置条件和不变量的相互作用。
李斯科夫的行为子类型概念定义了对象可替代性的概念；也就是说，如果S是T的子类型，那么程序中的T类型的对象可以被替换为S类型的对象，而不改变该程序的任何原定的属性（例如正确性）。
行为子类型是比类型理论中典型的函数子类型概念更强的概念，典型子类型仅依赖于自变量类型的差异和返回类型的协方差。行为子类型一般来说是不可判定的：如果q是“x的方法总是终止”的属性，那么程序（例如编译器）就不可能验证它对于T的某些子类型S是否成立，即使q对于T确实成立。尽管如此，该原理在类层次结构设计的推理中是有用的。
李斯科夫的原则对新的面向对象编程语言中采用的签名提出了一些标准要求（通常是在类而不是类型的层次上；请参见标称和结构子类型的区别）：
除了签名要求之外，子类型还必须满足许多行为条件。这些在一个类似于按合同方法设计的术语中有详细说明，导致对合同如何与继承交互的一些限制：
前置条件和后置条件的规则与伯特兰·迈耶（Bertrand Meyer）在1988年出版的《面向对象软件构建》一书中介绍的规则相同。迈耶和后来第一个使用行为亚类型这个术语的皮埃尔·爱美瑞克（Pierre America），都给出了一些行为亚类型概念的证明理论定义，但是他们的定义没有考虑到在支持引用或指针的编程语言中可能出现的混叠。考虑混叠是李斯科夫和荣格（1994）的主要改进，一个关键因素是历史约束。根据迈耶和爱美瑞克的定义，易变点是不变点的行为子类型，而LSP禁止这样做。
暂无