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

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

Аннотация

В статье используются разработанные группой 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. Определения

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

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

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

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

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

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

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

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

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

Попытаемся специфицировать типы описанных выше С++-реализаций 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 

---- 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),

[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) 

   h = GetWidth(f) = GetWidth(SetWidth(f1, w)) = w

---- 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