Поведенческий подтип

В объектно-ориентированном программировании поведенческое подтипирование — это принцип, согласно которому подклассы должны удовлетворять ожидания клиентов, обращающихся к объектам подкласса через ссылки типа суперкласса, не только в отношении синтаксической безопасности (например, отсутствия ошибок «метод не найден»), но и в отношении синтаксической безопасности. также в отношении правильности поведения. В частности, свойства, которые клиенты могут доказать с помощью спецификации предполагаемого типа объекта, должны сохраняться, даже если объект на самом деле является членом подтипа этого типа. ^[1]

Например, рассмотрим тип Stack и тип Queue , у которых есть метод put для добавления элемента и метод get для его удаления. Предположим, что в документации, связанной с этими типами, указано, что методы типа Stack должны вести себя ожидаемым образом для стеков (т. е. они должны демонстрировать поведение LIFO ), а методы типа Queue должны вести себя ожидаемым образом для очередей (т. е. они должны демонстрировать поведение FIFO ). Предположим теперь, что тип Stack объявлен как подкласс типа Queue. Большинство компиляторов языков программирования игнорируют документацию и выполняют только те проверки, которые необходимы для сохранения безопасности типов . Поскольку для каждого метода типа Queue тип Stack предоставляет метод с совпадающим именем и сигнатурой, эта проверка будет успешной. Однако клиенты, обращающиеся к объекту Stack через ссылку типа Queue, согласно документации Queue, ожидают поведения FIFO, но наблюдают поведение LIFO, что делает недействительными доказательства правильности этих клиентов и потенциально приводит к неправильному поведению программы в целом.

Этот пример нарушает поведенческий подтип, поскольку тип Stack не является поведенческим подтипом типа Queue: это не тот случай, когда поведение, описанное в документации типа Stack (т. е. поведение LIFO), соответствует документации типа Queue (которая требует поведения FIFO). .

Напротив, программа, в которой и Stack, и Queue являются подклассами типа Bag, спецификация которого для get заключается лишь в том, что она удаляет некоторый элемент, действительно удовлетворяет поведенческому подтипированию и позволяет клиентам безопасно рассуждать о правильности на основе предполагаемых типов объектов, которые они используют. взаимодействовать с. Действительно, любой объект, удовлетворяющий спецификации Stack или Queue, также удовлетворяет спецификации Bag.

Важно подчеркнуть, что является ли тип S поведенческим подтипом типа T, зависит только от спецификации ( т. е. документации ) типа T; реализация . типа T, если она есть, совершенно не имеет отношения к этому вопросу Действительно, тип T даже не обязательно должен иметь реализацию; это может быть чисто абстрактный класс. Другой пример: тип Stack выше является поведенческим подтипом типа Bag, даже если реализация типа Bag демонстрирует поведение FIFO: важно то, что в спецификации типа Bag не указано, какой элемент удаляется методом get . Это также означает, что поведенческие подтипы могут обсуждаться только в отношении конкретной (поведенческой) спецификации для каждого задействованного типа и что, если рассматриваемые типы не имеют четко определенной поведенческой спецификации, поведенческие подтипы не могут обсуждаться осмысленно.

Проверка поведенческих подтипов

Тип S является поведенческим подтипом типа T, если каждое поведение, разрешенное спецификацией S, также разрешено спецификацией T. Это требует, в частности, чтобы для каждого метода M из T спецификация M в S была сильнее, чем в Т.

Спецификация метода, заданная предусловием P s _и постусловием Q s _, сильнее, чем спецификация, заданная предусловием P _t и постусловием Q _t (формально: (P _s , Q _s ) ⇒ (P _t , Q _t )) если P _s слабее , чем P _t (т. е. P _t влечет за собой P _s ), а Q _s сильнее, чем Q _t (т. е. Q _s влечет за собой Q _t ). То есть усиление спецификации метода можно выполнить путем усиления постусловия и ослабления предусловия. Действительно, спецификация метода является более сильной, если она накладывает более конкретные ограничения на выходные данные для входных данных, которые уже поддерживались, или если для поддержки требуется больше входных данных.

Например, рассмотрим (очень слабую) спецификацию метода, который вычисляет абсолютное значение аргумента x , определяющего предварительное условие 0 ≤ x и постусловие 0 ≤ результат. В этой спецификации говорится, что методу не обязательно поддерживать отрицательные значения x , и ему нужно только гарантировать, что результат также неотрицательен. Два возможных способа усилить эту спецификацию — усилить постусловие, чтобы указать результат = |x|, т. е. результат равен абсолютному значению x, или ослабить предварительное условие до «истины», т. е. все значения x. должны поддерживаться . Конечно, мы также можем объединить и то, и другое в спецификацию, в которой говорится, что результат должен равняться абсолютному значению x для любого значения x .

Однако обратите внимание, что можно усилить спецификацию ((Ps _, Qs ₎ ⇒ (Pt _, Qt ₎ ) без усиления постусловия (Qs _⇏ Qt ₎ . ^[2]^[3] Рассмотрим спецификацию метода абсолютного значения, которая задает предусловие 0 ≤ x и результат постусловия = x. Спецификация, определяющая предусловие «истина» и результат постусловия = |x| усиливает эту спецификацию, хотя результат постусловия = |x| не усиливает (или ослабляет) постусловие result = x. Необходимым условием для того, чтобы спецификация с предусловием P _s и постусловием Q _s была более сильной, чем спецификация с предусловием P _t и постусловием Q _t, является то, что P _s слабее, чем P _t , и "Q _s или не P _s " сильнее, чем " Q _т или нет П _т ". Действительно, «результат = |x| или ложь» усиливает «результат = x или x < 0».

«Заменяемость»

В влиятельном программном выступлении ^[4] Об абстракции данных и иерархиях классов на исследовательской конференции по языкам программирования OOPSLA 1987 года Барбара Лисков сказала следующее: «Здесь требуется что-то вроде следующего свойства подстановки: Если для каждого объекта $o_{1}$ типа S есть объект $o_{2}$ типа Т такой, что для всехпрограмм P, определенных в терминах T, поведение P не меняется, когда $o_{1}$ заменяетсядля $o_{2}$ , то S является подтипом T». Эта характеристика с тех пор широко известна как принцип замены Лискова (LSP) . Однако, к сожалению, у нее есть несколько проблем. Во-первых, в своей первоначальной формулировке она слишком строга: мы редко хотим поведение подкласса должно быть идентично поведению его суперкласса; замена объекта суперкласса объектом подкласса часто делается с намерением изменить поведение программы, хотя, если соблюдается поведенческое подтипирование, таким образом, чтобы сохранить желаемое поведение программы. Во-вторых, здесь не упоминаются спецификации , что приводит к неправильному прочтению, когда реализация типа S сравнивается с реализацией типа T. Это проблематично по нескольким причинам, одна из которых заключается в том, что он не поддерживает общий случай, когда. T абстрактен и не имеет реализации. В-третьих, и это наиболее тонко, в контексте объектно-ориентированного императивного программирования трудно точно определить, что означает универсальное или экзистенциальное количественное определение объектов данного типа или замена одного объекта. другой. ^[3] В приведенном выше примере мы не заменяем объект Bag объектом Stack, мы просто используем объект Stack в качестве объекта Bag.

В интервью 2016 года сама Лисков объясняет, что то, что она представила в своем программном выступлении, было «неформальным правилом», которое позже предложила Жаннетт Винг «попытаться точно выяснить, что это значит», что привело к их совместной публикации. ^[1] о поведенческих подтипах, и действительно, «технически это называется поведенческим подтипами». ^[5] Во время интервью она не использует замещающую терминологию для обсуждения концепций.

Примечания

^ Перейти обратно: ^а ^б Лисков, Варвара; Винг, Жаннетт (1 ноября 1994 г.). «Поведенческое понятие подтипирования» . Транзакции ACM в языках и системах программирования . 16 (6): 1811–1841. дои : 10.1145/197320.197383 .
^ Паркинсон, Мэтью Дж. (2005). Локальные рассуждения для Java (PDF) (доктор философии). Кембриджский университет.
^ Перейти обратно: ^а ^б Ливенс, Гэри Т.; Науманн, Дэвид А. (август 2015 г.). «Поведенческое подтипирование, наследование спецификаций и модульное мышление» . Транзакции ACM в языках и системах программирования . 37 (4). дои : 10.1145/2766446 .
^ Лисков, Б. (май 1988 г.). «Основной доклад – абстракция данных и иерархия» . Уведомления ACM SIGPLAN . 23 (5): 17–34. дои : 10.1145/62139.62141 .
^ ван Флек, Том (20 апреля 2016 г.). Интервью с Барбарой Лисковой . АКМ. Архивировано из оригинала 21 декабря 2021 г.

Ссылки

Паркинсон, Мэтью Дж.; Бирман, Гэвин М. (январь 2008 г.). «Логика разделения, абстракция и наследование». Уведомления ACM SIGPLAN . 43 (1): 75–86. дои : 10.1145/1328897.1328451 .

[liskov1994-1] Перейти обратно: ^а ^б Лисков, Варвара; Винг, Жаннетт (1 ноября 1994 г.). «Поведенческое понятие подтипирования» . Транзакции ACM в языках и системах программирования . 16 (6): 1811–1841. дои : 10.1145/197320.197383 .

[2] Паркинсон, Мэтью Дж. (2005). Локальные рассуждения для Java (PDF) (доктор философии). Кембриджский университет.

[leavens2015-3] Перейти обратно: ^а ^б Ливенс, Гэри Т.; Науманн, Дэвид А. (август 2015 г.). «Поведенческое подтипирование, наследование спецификаций и модульное мышление» . Транзакции ACM в языках и системах программирования . 37 (4). дои : 10.1145/2766446 .

[4] Лисков, Б. (май 1988 г.). «Основной доклад – абстракция данных и иерархия» . Уведомления ACM SIGPLAN . 23 (5): 17–34. дои : 10.1145/62139.62141 .

[5] ван Флек, Том (20 апреля 2016 г.). Интервью с Барбарой Лисковой . АКМ. Архивировано из оригинала 21 декабря 2021 г.

[1]

[2]

[3]

[4]

[5]