История изменений

LSP - это формализм теории типов, почитай документ выше. Там всё формально описано, включая имеющиеся ограничения

На первой же странице даётся самое финальное свойство (к которому идёт весь текст и заканчивается на последней странице):

Let q(x) be a property provable about object x of type T. Then q(y) should be true for objects y of type S where S is a subtype of T"

Здесь и дальше речь идёт именно о «propery provable about», а не «property of»

В разделе model of computation идёт описание модели, в которой тип задаётся через тройку (объекты, значения, методы), где методы бывают одного из трёх типов: мутаторы, обсерверы и продюсеры. Заметь, что «проверяемые ограничения» не являются частю модели вычислений

Практическая запись типа - имя, инварианты, ограничения, история и методы. Методы - имя-сигнатура и тройка requires+modifies+ensures.

В смысле доказательства «property provable about» интересны инварианты и ограничения,

инварианты (в отдельной секции) задаются как предикаты, которые _любым_ образом задают легальные значения (или являются конъюнкцией других инвариантов из этого типа и универсального множества значений). Если ни один инвариант явно не задан, то используется инвариант по умолчанию, равный true.

ограничения (тоже есть отдельная глава). Там важно history rule, которое говорит что для любого мутатора i, если он срабатывает (выполняются пре и пост условия), то и в подклассе они тоже срабатывают. Это одна из фишек введенная именно в LSP. Но так как подтип может объявить свои мутаторы, к этому правилу добавляется дополнение: подтип не должен иметь таких мутаторов, которые вели бы себя по-другому, чем в надтипе. На основе этого выводится понятия ограничений, которые говорят что для всей области определения должно выполняться некое утверждение, причём способ задания этого утверждения не описан - он может быть любым, и уж точно он не обязан является одним из методов

дальше на «figure 4» даётся определение того, что есть подтип, и нам тут важно в пункте 2 «constraint rule»: наличие ограничения на подтипе означает наличие того же ограничения на надтипе

в методах, тройка requires-modifies-ensures задаёт проверки на типы, относительно modifies свойств, к которым будут применяться описанная выше схема, и это смысл человекочитаемой фразы «about x» в фразе «provable about x»

таким образом, мы можем придумать любые «тесты» («важные для системы свойства») относительно которых будет проверяться поведение типа и подтипа - главное, чтобы они казались нам почему-то важными

как раз то, о чём говорит monk

ну и да, рефлекшен всё это ломает, поэтому если на вопрос из ОП-поста отвечаешь, что соблюдаешь LSP, это автоматически означает, что ты не пользуешься рефлексией

LSP - это формализм теории типов, почитай документ выше. Там всё формально описано, включая имеющиеся ограничения

На первой же странице даётся самое финальное свойство (к которому идёт весь текст и заканчивается на последней странице):

Let q(x) be a property provable about object x of type T. Then q(y) should be true for objects y of type S where S is a subtype of T"

Здесь и дальше речь идёт именно о «propery provable about», а не «property of»

В разделе model of computation идёт описание модели, в которой тип задаётся через тройку (объекты, значения, методы), где методы бывают одного из трёх типов: мутаторы, обсерверы и продюсеры. Заметь, что «проверяемые ограничения» не являются частю модели вычислений

Практическая запись типа - имя, инварианты, ограничения, история и методы. Методы - ия-сигнатура и тройка requires+modifies+ensures.

В смысле доказательства «property provable about» интересны инварианты и ограничения,

инварианты (в отдельной секции) задаются как предикаты, которые _любым_ образом задают легальные значения (или являются конъюнкцией других инвариантов из этого типа и универсального множества значений). Если ни один инвариант явно не задан, то используется инвариант по умолчанию, равный true.

ограничения (тоже есть отдельная глава). Там важно history rule, которое говорит что для любого мутатора i, если он срабатывает (выполняются пре и пост условия), то и в подклассе они тоже срабатывают. Это одна из фишек введенная именно в LSP. Но так как подтип может объявить свои мутаторы, к этому правилу добавляется дополнение: подтип не должен иметь таких мутаторов, которые вели бы себя по-другому, чем в надтипе. На основе этого выводится понятия ограничений, которые говорят что для всей области определения должно выполняться некое утверждение, причём способ задания этого утверждения не описан - он может быть любым, и уж точно он не является одним из методов

дальше на «figure 4» даётся определение того, что есть подтип, и нам тут важно в пункте 2 «constraint rule»: наличие ограничения на подтипе означает наличие того же ограничения на надтипе

в методах, тройка requires-modifies-ensures задаёт проверки на типы, относительно modifies свойств, к которым будут применяться описанная выше схема, и это смысл человекочитаемой фразы «about x» в фразе «provable about x»

таким образом, мы можем придумать любые «тесты» («важные для системы свойства») относительно которых будет проверяться поведение типа и подтипа - главное, чтобы они казались нам почему-то важными

как раз то, о чём говорит monk

ну и да, рефлекшен всё это ломает, поэтому если на вопрос из ОП-поста отвечаешь, что соблюдаешь LSP, это автоматически означает, что ты не пользуешься рефлексией