Logo Море(!) аналитической информации!
IT-консалтинг Software Engineering Программирование СУБД Безопасность Internet Сети Операционные системы Hardware
VPS/VDS серверы. 30 локаций на выбор

Серверы VPS/VDS с большим диском

Хорошие условия для реселлеров

4VPS.SU - VPS в 17-ти странах

2Gbit/s безлимит

Современное железо!

Бесплатный конструктор сайтов и Landing Page

Хостинг с DDoS защитой от 2.5$ + Бесплатный SSL и Домен

SSD VPS в Нидерландах под различные задачи от 2.6$

✅ Дешевый VPS-хостинг на AMD EPYC: 1vCore, 3GB DDR4, 15GB NVMe всего за €3,50!

🔥 Anti-DDoS защита 12 Тбит/с!

2010 г.

Об одном примере нарушения принципа подстановки Лисков

А.Г. Пискунов, С.М. Петренко

Аннотация

В статье используются разработанные группой RDG (RAISE Development Group) приемы RAISE Development Method для анализа примера Роберта Мартина (Robert C. Martin), который иллюстрирует принцип подстановки Барбары Лисков (Barbara Liskov). Кроме того, применяется технический прием проектирования RDG (впервые упомянутый Джоном Гуттагом (John V. Guttag)), дополняющий принципы дизайна по контракту.

Содержание

Аннотация
1. Введение
2. Определения
3. Спецификации типов примера
3.1. Тип Rectangle
3.2. Тип Square
4. Пример нарушения принципа подстановки
5. Уточнение терминов
Ссылки

1. Введение

Принцип подстановки Лисков помогает понять суть термина suptyping – выделение подтипа, а статья Роберта Мартина [5] показывает некоторое несоответствие между наследованием в языке C++ и выделением подтипа. В этой статье принцип формулируется следующим образом:

If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2 then S is a subtype of T.

Перевод может звучать как-то так:

Если для каждого объекта o1 типа S существует объект o2 типа T, такой что любая программа P, определенная в терминах T, не изменяет своего поведения при подстановке объекта o1 вместо объекта o2, то тип S является подтипом T.
Эта формулировка допускает достаточно неоднозначную трактовку. Чтобы понять, что имеется в виду, рассмотрим пример из статьи с прямоугольниками и квадратами.

Определим родительский класс Rectangle:

---- File:./rsl/rectangle.cpp

class Rectangle{
  public:
    virtual void SetWidth(double w){itsWidth=w;}
    virtual void SetHeight(double h) {itsHeight=H;}
    double GetHeight() const {return itsHeight;}
    double GetWidth()  const {return itsWidth;}
  private:
    double itsWidth;
    double itsHeight;
};

 ---- End Of File:./rsl/rectangle.cpp 

и наследуем от него класс Square:

---- File:./rsl/square.cpp

class Square : Rectangle {
  public:
    virtual void SetWidth(double w);
    virtual void SetHeight(double h);
};
void Square::SetWidth(double w){
  Rectangle::SetWidth(w);
  Rectangle::SetHeight(w);
}
void Square::SetHeight(double h){
  Rectangle::SetHeight(h);
  Rectangle::SetWidth(h);
}

 ---- End Of File:./rsl/square.cpp 

Автор статьи не без основания утверждает, что в приведенном примере в фукнции LSPV таки нарушается принцип подстановки:

---- File:./rsl/violation.cpp

void LSPV(Rectangle& r){
  r.SetWidth(5);
  r.SetHeight(4);
  assert(r.GetWidth() * r.GetHeight()) == 20);
}

---- End Of File:./rsl/violation.cpp 

Можно было бы возразить автору, что принцип подстановки плохо сформулирован, что не определен термин замена (хотя в данном примере все понятно: в программу передается ссылка на объект подкласса), что непонятен термин поведение программы и так далее.

Но попробуем проанализировать пример с точки зрения методов RDG [3] и придать точный теоретико-множественный смысл этим и некоторым другим терминам.

2. Определения

Начнем с определения термина типа. За основу возмем определение термина абстрактный тип данных (АТД), данное Бертраном Мейером (Bertrand Meyer) [2].

Спецификация АТД состоит из четырех разделов:

  • типы;
  • сигнатуры функций;
  • аксиомы функций и типов;
  • предусловия применения частично определенных функций.

Далее будем придерживаться следующих соглашений:

  • саму спецификацию будем называть типом;
  • доменом типа будем называть множество всех величин данного типа, то есть величин, удовлетворяющих спецификации;
  • в разделе типы (по Мейеру) будут содержаться обозначение домена типа, аксиомы для его описания, а также, возможно, спецификации простых вспомогательных типов;
  • в разделе функций будут вводиться сигнатуры функций, предусловия и постусловия применения функций; из всего набора функций выделяются функции-генераторы (generator, на выходе имеется обозначение домена типа) и функции-наблюдатели (observer, на выходе функции отсутствует обозначение домена типа); особенно важную роль играют функции, не выводимые из других функции;
  • в разделе аксиом будут определяться аксиомы, описывающие попарное применение функций-генераторов и функций-наблюдателей.

В простых и привычных случаях , когда это не приводит к путанице, типом можно называть домен типа. Например, можно называть типом прямое произведение двух множеств A × B, подразумевая, что имеется спецификация функций проекции. Обозначение A × B, мыслимое без функций проекции – это домен типа, A × B, мыслимое вместе с аксиомами функций проекции, – это тип.

Далее, уточним следующее определение Мейера [1]:

Класс – это абстрактный тип данных, поставляемый с возможно частичной реализацией.

Спецификация (то есть тип), в которой произведена замена аксиом, описывающих попарное поведение функций, на частично определенные функции, будем называть аппликативной реализацией. Определение класса на языке программирования L, удовлетворяющее требованиям спецификации, будет называть (обычно, императивной) L-реализацией.

3. Спецификации типов примера

Вопросы единственности типов, полноты типов (в смысле полноты системы аксиом), противоречивости типов (в смысле противоречивости системы аксиом), единственности реализации, оптимальности спецификации и реализаций, синтаксического сахара RSL и др. здесь не рассматриваются.

Попытаемся специфицировать типы описанных выше С++-реализаций Rectangle и Square на языке формальных спецификаций RSL в соответствии с методом, принятым в RDG. Дополнительный тип UReal (домен которого включает все положительные вещественные значения) вводится, чтобы функции были всюду определены, и не нужно было заниматься предусловиями.

3.1. Тип Rectangle

Аксиомы gw_sw и gh_sh очевидны: что положил, то и получил назад. Аксиомы gw_sh и gh_sw означают независимость высоты от ширины в значениях множества Figure, соответствующих спецификации Rectangle. Например, для любого f: Figure значения, возвращаемые функцией GetWidth не зависят от применения функции SetHight.

---- File:./rsl/rectangle.rsl

scheme Rectangle =  class
    type                        
      Figure,
      UReal  =  {| r: Real :- r > 0.0 |}  
    value
      SetWidth  : Figure >< UReal -> Figure,
      SetHeight : Figure >< UReal -> Figure, 
      GetWidth  : Figure          -> UReal,
      GetHeight : Figure          -> UReal     
    axiom
      [gw_sw]
        all w: UReal, f: Figure:- GetWidth(SetWidth(f, w)) = w,
      [gw_sh]
        all h: UReal, f: Figure:- GetWidth(SetHeight(f, h)) = GetWidth(f),
      [gh_sh]
        all h: UReal, f: Figure:- GetHeight(SetHeight(f, h)) = h,
      [gh_sw]
        all w: UReal, f: Figure:- GetHeight(SetWidth(f, w)) = GetHeight(f)
  end
   
---- End Of File:./rsl/rectangle.rsl 

Аппликативная реализация типа Rectangle может иметь следующий вид:

---- File:./rsl/ar.rsl

scheme AR =  class
    type
      Figure = UReal >< UReal,
      UReal  =  {| r: Real :- r > 0.0 |}
    value
      SetWidth  : Figure >< UReal -> Figure
       SetWidth ((h, w), v) is  (h, v),
      SetHeight : Figure >< UReal -> Figure
       SetHeight ((h, w), v) is  (v, w),
      GetWidth  : Figure          -> UReal
       GetWidth (h, w) is  w,
      GetHeight : Figure          -> UReal
       GetHeight (h, w) is  h
  end
---- End Of File:./rsl/ar.rsl 

Домен типа Rectangle (множество Figure) объявляется как прямое произведение UReal × UReal, функции GetWidth и GetHeight – проекции.

3.2. Тип Square

В типе Square, предположительно являющемся подтипом Rectangle, аксиомы gw_sh и gh_sw имеют смысл, строго противоположный смыслу аналогичных аксиом в Rectangle:

---- File:./rsl/square.rsl

scheme Square =  class
    type
      Figure,
      UReal  =  {| r: Real :- r > 0.0 |}
    value
      SetWidth  : Figure >< UReal -> Figure,
      SetHeight : Figure >< UReal -> Figure,
      GetWidth  : Figure          -> UReal,
      GetHeight : Figure          -> UReal
    axiom
      [gw_sw]
        all w: UReal, f: Figure:- GetWidth(SetWidth(f, w))= w,
      [gw_sh]
        all h: UReal, f: Figure:- GetWidth(SetHeight(f, h)) = h,
      [gh_sh]
        all h: UReal, f: Figure:- GetHeight(SetHeight(f, h)) = h,
      [gh_sw]
        all w: UReal, f: Figure:- GetHeight(SetWidth(f, w)) = w
  end

---- End Of File:./rsl/square.rsl 
Вот аппликативная реализаци типа Square, записанная в форме наследования:
---- File:./rsl/as.rsl

AR
scheme AS = extend  hide  SetWidth, SetHeight in AR  with  class
    value
      SetWidth  : Figure >< UReal -> Figure
       SetWidth ((h, w), v) is  (v, v),
      SetHeight : Figure >< UReal -> Figure
       SetHeight ((h, w), v) is  (v, v)
  end
  
---- End Of File:./rsl/as.rsl 

В новом классе AS "наследуется" (extend) все из класса AR, но при этом "прячутся" (hide) родительские функции SetWidth, SetHeight и объявляются свои.

4. Пример нарушения принципа подстановки

Специфицируем на RSL аппликативную реализацию С++-функции LSVP, приводимой во введении для иллюстрации нарушения принципа подстановки. Спецификация этой функции могла бы выглядеть следующим образом:

---- File:./rsl/v.rsl
AS
scheme V = extend  AS  with  class
    value
      LSPV : Figure >< (Figure >< UReal -> Figure)  -> Unit
       LSPV (r, setWidth) is
        let f = SetHeight(setWidth(r,5.0),4.0),
            w = GetWidth (f),
            h = GetHeight(f) in
            if ( h * w = 20.0) then skip else chaos end
        end
--       pre
--        (all h: UReal:- GetWidth(SetHeight(setWidth(r,5.0), h)) = GetWidth(setWidth(r,5.0)))

  end

---- End Of File:./rsl/v.rsl 

Аппликативная реализация функции LSPV делает точно то же, что и C++-реализация. Функция последовательно применяет функции setWidth и SetHeight к полученной на вход переменной r: Figure и, если произведение высоты r на длину r полученного прямоугольника не равняется 20, ведет себя хаотическим, неопределенным образом (chaos). Чтобы подчеркнуть наличие ошибки, в комментарии написано предусловие этой частично определенной функции LSPV, хотя в сигнатуре она описана как полностью определенная.

Честно говоря, доводы Мартина насчет того, что его пример демонстрирует реальную проблему, выглядят не слишком убедительно:

So here is the real problem: Was the programmer who wrote that function justified in assuming that changing the width of a Rectangle leaves its height unchanged? Clearly, the programmer of LSPV made this very reasonable assumption.

Здесь имеется реальная проблема: Оправданным ли образом программист, написавший эту функцию, полагал, что при изменении длины прямогульника его высота остается неизменной? Яcно, что программист функции LSPV сделал вполне осмысленное предположение.

То есть Мартин считает, что этого программиста осуждать не за что. И это действительно так, но здесь нет никакой проблемы. Программист, использующий класс Rectangle, должен делать только те предположения об используемом классе, которые соответствуют спецификации класса. Формально говоря, функция LSPV при получении на вход переменной a: Square сделала то, что от нее и требовалось. Поэтому нельзя говорить об изменении поведения LSPV. Вот если бы была написана хотя бы частичная спецификация этой функции, если хотя бы было указано, что LSPV – это всюду определенная функция (LSPV : Rectangle → Unit), а при получении a: Square она бы повисла, то есть оказалась бы не всюду определенной, то это была бы действительно проблема несоответствия реализации спецификации.

Наличие аппликативной реализации и C++ -реализации, приводящих к одинаковым трудностям, говорит о том, что дело здесь не в языке реализации.

5. Уточнение терминов

Под термином выделение типа (subtyping) будем понимать добавление к супертипу непротиворечивых уточнений. Слово уточнение здесь означает, что все предыдущие свойства типа должны сохраняться. Система аксиом для домена и функций должна оставаться непротиворечивой. Домен типа не может расшириться. Функции могут быть инкапсулироваться (удаляться из описания), добавляться или переопределяться (т.е. в спецификации подтипа может быть удалена некоторая функция супертипа и добавлена своя с той же сигнатурой), но аксиомы супертипа должны выполняться.

То есть требуется уточнение спецификации типа в соответствии с принципами проектирования по контракту [4].

В нашем случае предположим, что тип Square является подтипом типа Rectangle. Тогда в типе-потомке должны одновременно выполняться обе версии аксиом gw_sh, одна из Rectangle:

[gw_sh]
   all h: UReal, f: Figure:- GetWidth(SetHeight(f, h)) = GetWidth(f),
вторая из Square:
[gw_sh]
   all h: UReal, f: Figure:- GetWidth(SetHeight(f, h)) = h

То есть в совокупности мы получаем следующую аксиому:

   all h: UReal, f: Figure:-
           h =   GetWidth(SetHeight(f, h))   /\
                 GetWidth(SetHeight(f, h)) = GetWidth(f) 
Отсюда следует аксиома:
   all h: UReal, f: Figure:-  h  = GetWidth(f) 
Однако если мы возьмем в UReal некоторое значение w, такое что wh, то по аксиоме gw_sw получим:
   h = GetWidth(f) = GetWidth(SetWidth(f1, w)) = w

Полученное противоречие показывает, что две разные версии аксиом gw_sh не могут выполняться вместе. Отсюда следует, что нет никакой возможности в принципе считать Square подтипом Rectangle. Их можно считать "братьями", являющимися подтипами некоторого неполного, неоднозначного типа.

К этому же заключению можно придти на основе того наблюдения, что можно написать С++-реализацию Square, от которой унаследовать С++-реализацию Rectangle. Было бы очень странно иметь в языке возможность наследования супертипа от подтипа.

В заключение специфицируем неполностью определенный тип с удаленными аксиомами gw_sh и gh_sw, являющийся настоящим родителем обоих классов:

---- File:./rsl/realdad.rsl

scheme RealDad =  class
    type
      Figure,
      UReal  =  {| r: Real :- r > 0.0 |}
    value
      SetWidth  : Figure >< UReal -> Figure,
      SetHeight : Figure >< UReal -> Figure,
      GetWidth  : Figure          -> UReal,
      GetHeight : Figure          -> UReal
    axiom
      [gw_sw]
        all w: UReal, f: Figure:- GetWidth(SetWidth(f, w)) = w,
      [gh_sh]
        all h: UReal, f: Figure:- GetHeight(SetHeight(f, h)) = h
  end

---- End Of File:./rsl/realdad.rsl 
С++-реализация этого типа может выглядеть следующим образом:
---- File:./rsl/realdad.cpp

class RealDad{
  public:
    virtual void SetWidth(double w)=0;
    virtual void SetHeight(double h)=0;
    double GetHeight() const {return itsHeight;}
    double GetWidth()  const {return itsWidth;}
  private:
    double itsWidth;
    double itsHeight;
};

 ---- End Of File:./rsl/realdad.cpp 

Оба класса Square и Rectangle должны наследоваться от класса RealDad, который и следует использовать для написания полиморфных функций вроде LSPV в качестве типа формального параметра.

Кроме того, нужно сказать, что принцип подстановки Лисков в формулировке 1994 года [6] выглядит лучше:

Let φ(x) be a property provable about objects x of type T. Then φ(y) should be true for objects y of type S where S is a subtype of T.
Пусть φ(x) – это свойство, доказываемое для объектов x типа T. Тогда свойством φ(x) должны обладать объекты y типа S, где S является подтипом T.

Ссылки

  1. Бертран Мейер. Основы объектно-ориентированного программирования. Статические структуры: классы.
  2. Бертран Мейер. Основы объектно-ориентированного программирования. Абстрактные типы данных (АТД).
  3. А.Г. Пискунов. The RAISE Method Group: Алгебраическое проектирование класса , 2007.
  4. Bertrand Meyer. Основы объектно-ориентированного программирования. Техника наследования.
  5. Robert C.Martin. The Liskov Substitution Principle. C++ Report, March 1996.
  6. Barbara H. Liskov, Jeannette M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, Volume 16 Issue 6, Nov. 1994.

VPS в России, Европе и США

Бесплатная поддержка и администрирование

Оплата российскими и международными картами

🔥 VPS до 5.7 ГГц под любые задачи с AntiDDoS в 7 локациях

💸 Гифткод CITFORUM (250р на баланс) и попробуйте уже сейчас!

🛒 Скидка 15% на первый платеж (в течение 24ч)

Скидка до 20% на услуги дата-центра. Аренда серверной стойки. Colocation от 1U!

Миграция в облако #SotelCloud. Виртуальный сервер в облаке. Выбрать конфигурацию на сайте!

Виртуальная АТС для вашего бизнеса. Приветственные бонусы для новых клиентов!

Виртуальные VPS серверы в РФ и ЕС

Dedicated серверы в РФ и ЕС

По промокоду CITFORUM скидка 30% на заказ VPS\VDS

Новости мира IT:

Архив новостей

IT-консалтинг Software Engineering Программирование СУБД Безопасность Internet Сети Операционные системы Hardware

Информация для рекламодателей PR-акции, размещение рекламы — adv@citforum.ru,
тел. +7 495 7861149
Пресс-релизы — pr@citforum.ru
Обратная связь
Информация для авторов
Rambler's Top100 TopList This Web server launched on February 24, 1997
Copyright © 1997-2000 CIT, © 2001-2019 CIT Forum
Внимание! Любой из материалов, опубликованных на этом сервере, не может быть воспроизведен в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав. Подробнее...