Уточнение терминов
Под термином выделение типа (subtyping) будем понимать добавление к супертипу непротиворечивых уточнений. Слово уточнение здесь означает, что все предыдущие свойства типа должны сохраняться. Система аксиом для домена и функций должна оставаться непротиворечивой. Домен типа не может расшириться. Функции могут быть инкапсулироваться (удаляться из описания), добавляться или переопределяться (т.е. в спецификации подтипа может быть удалена некоторая функция супертипа и добавлена своя с той же сигнатурой), но аксиомы супертипа должны выполняться.
То есть требуется уточнение спецификации типа в соответствии с принципами проектирования по контракту [].
В нашем случае предположим, что тип 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, такое что w ? h, то по аксиоме 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 года [] выглядит лучше: 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.
