нарушения принципа подстановки
Специфицируем на 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++ -реализации, приводящих к одинаковым трудностям, говорит о том, что дело здесь не в языке реализации.
