قاعده جانشانی لیسکوف

تعویض پذیری یک اصل در برنامه نویسی شیءگرا است که می گوید در یک برنامهٔ رایانه ای ، اگر S زیرنوع T باشد، امکان جایگزینی نمونه های نوع T با نمونه های نوع S وجود دارد. یعنی بدون این که هیچکدام از ویژگی های مطلوب برنامه ( اعم از درستی، ماهیت کار انجام شده توسط برنامه و . . . ) تغییر کند؛ می توان یک شیء از نوع T با هر شیءای از نوع S را جایگزین کرد. به بیان رسمی تر، اصل جایگزینی لیسکوف ( LSP ) تعریف خاصی از یک رابطهٔ زیرنوعی به نام رابطهٔ ( قوی ) زیرنوعی رفتاری است، که در ابتدا توسط باربارا لیسکوف در یک سخنرانی در کنفرانسی در سال ۱۹۷۸ با عنوان انتزاع داده ها و سلسله مراتب معرفی شد. این قاعده یک رابطهٔ معنایی است ( نه صرفاً نحوی ) ، زیرا هدف آن تضمین قابلیت جانشانی انواع در یک ساختار سلسله مراتبی است. باربارا لیسکوف و جینت وینگ به طور خلاصه در مقاله ای منتشر شده در سال ۱۹۹۴ توضیح دادند:
نیازمندی های زیرنوع: اگر ϕ ( x ) یک ویژگی قابل اثبات برای انواع x از نوع T باشد؛ آنگاه ϕ ( y ) برای تمام y هایی از نوع S که S زیرنوعی از T است؛ باید صحیح باشد.
در همان مقاله، لیسکوف و وینگ منظور خود را از ساختار «انوع رفتاری» به وسیلهٔ گسترشی از منطق Hoare - که شباهت خاصی به «طراحی براساس قرارداد» برترند میر دارد - به تفصیل شرح داده اند که در آن تعامل با زیرنوع ها به شکل پیش شرط ها، پس شرط ها و ناوردا توضیح داده می شود.
مفهوم لیسکوف از یک «زیرنوع رفتاری» مفهومی از جایگزینی برای اشیا را تعریف می کند. یعنی اگر S زیرنوع T باشد، ممکن است اشیاء از نوع T در یک برنامه با اشیاء از نوع S جایگزین شوند؛ به شکلی که هیچ یک از خصوصیات مطلوب آن برنامه ( مانند درستی ) تغییر پیدا نکند.
رابطهٔ زیرنوعیِ رفتاری یک مفهوم قوی تر از زیرنوعی معمولی توابع تعریف شده در نظریهٔ نوع ها است؛ که فقط به پادوردایی انواع آرگومان ها و هم وردایی نوع برگشتی متکی است. زیرنوعیِ رفتاری به طور کلی تصمیم ناپذیر است: اگر q ویژگیِ «متد x همیشه خاتمه می یابد» باشد؛ آنگاه تأیید این ویژگی برای برخی انواع S که زیرنوع T هستند برای یک برنامهٔ رایانه ای ( مانند یک مترجم ) ناممکن است ( حتی در صورتی که ویژگی فوق برای T صحیح باشد ) . با این وجود این اصل در طراحی سلسله مراتب اشتقاق مفید است.
اصل لیسکوف برخی نیازمندی های استاندارد را برای امضای انواع در زبان های برنامه نویسی جدید شیءگرا الزام می کند ( معمولاً در سطح کلاس ها و نه انواع. برای دیدن تمایز بین این دو مراجعه کنید به زیرنوع نامی و ساختاری ) :