stalcer,
> ПК>2) Математические понятия квадрата и прямоугольника не предполагают от них > ПК>никакого поведения, соответственно, эти понятия в программе, наделяющей > ПК>соответствующие объекты поведением, могут использоваться очень ограниченно.
> Очень даже предполагают, имхо. Они задают инварианты, которые определяют, > в какой степени можно менять свойства экземпляра того или иного понятия.
Да, инварианты они определяют. Т.е. они говорят о наборе валидных состояний.
Чем они не наделяют экземпляры понятий, так это возможностью переходить из одного
состояния в другое, т.к. идентифицируют свои экземпляры понятий с тем же, с чем
идентифицируется состояние объекта в программировании. Трансформация квадрата или
прямоугольника приводит к получению нового экземпляра понятия (квадрата
или прямоугольника), а не к изменению существующего.
Т.е., собственно, в математике (по крайней мере, в части, определяющей квадраты
как разновидность прямоугольников) нет изменения. Есть математические объекты,
задаваемые их свойствами. "Два" квадрата, коль скоро доказано, что они обладают
одними и теми же свойствами, -- суть один математический объект. То же в случае
векторов, точек и т.п. Т.е. нет как такового изменения экземпляров, есть их
создание (или выделение, как, пожалуй, более точно выразился Владимир в
соседней подветке).
Скажем, как можно изменить числа "5" или "10"? Для математики квадраты,
прямоугольники, точки, вектора и т.п. в этом смысле -- более-менее то же самое.
Они идентифицируют некоторое значение в множестве возможных.
Программирование же построено поверх этой модели, и добавляет к объекту понятие
identity, которое не зависит от состояния объекта: два объекта, даже находящихся
в одном состоянии, тем не менее, остаются двумя разными объектами.
Т.е., для нашего случая как раз принципиальна разница между программированием
и математикой в определении identity объектов.
> ПК>3) И да, понятия в программировании далеко не обязательно один-в один > ПК>соответствуют понятиям предметной области.
> Но, ведь проблема-то как раз в том, чтобы найти способ как можно болеепохожего описания.
Не факт.
> s>> На самом деле, в математиеских изысканиях, мы оперируем понятиямиs>> точно также, как объектами в программе. Например, в ходе логического > s>> доказательства теоремы мы также "читаем" свойства понятий и также > s>> изменяем их.
> ПК>Относительно изменения есть серьезные сомнения...
> Если их нигде не изменять (как минимум — задавать), то зачем же их вообще > читать?
Можно говорить не об изменении существущих экземпляров, а о создании новых.
Так, например, происходит в случае "чистого" функционального программирования,
которое в этом смысле как раз достаточно близко к математике.
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
Здравствуйте, stalcer, Вы писали:
S>1) ООП придумано, чтобы писать программы в терминах предметной области. S>2) Принцип подстановки Лисков — один из принципов ООП. S>3) С точки зрения нашей предметной области (математики) любой квадрат является прямоугольником. S>4) Вся эта ветка форума показывает, что квадрат от прямоугольника наследовать нельзя, так как нарушается ППЛ.
В пункте 4 ошибка. Его таки можно пронаследовать так, чтобы ППЛ не нарушился, если операции не будут изменять состояния объекта.
S>Налицо явное противоречие. Значит один из пунктов неверный. S>Подозреваю, нас злостно обманывали в школе и это пункт 3.
S>На самом деле, в математиеских изысканиях, мы оперируем понятиями точно также, как объектами в программе.
Не точно также. Понятие подмножества в математике и понятие "подтипа" в computer scienсe — разные вещи.
1) Абстрактый Тип Данных (АТД) определяется только набором операций над ним, и никоим образом не атрибутами. Операция определяется предусловиями и постусловиями. При этом, у АТД все равно есть множество возможных значений, и множество значений подтипа является подмножеством множества значений типа. Вот это, последнее — единственная общая черта, и это необходимое, но совсем не достаточное условие.
2) А вот это серьезное отличие: у наших объектов есть состояние и модифицирующие операции (нонсенс с точки зрения математики — она вообще под таким углом на проблему не смотрит), и модифицирующие операции у нас являются замкнутыми, т.е. не могут выводить объект из его типа.
В принципе пункта 2 достаточно, чтобы разрешить "явное противоречие". А именно, из того факта, что одно множесто является подмножеством другого, вовсе не следует, что они связаны отношением подтипа. Причина нарушения ППЛ в нашем случае состоит именно в том, что операции изменения размеров не являются замкнутыми — они выводят квадрат из класса квадратов. Как заканчивались наставления самураев по владению техникой меча, это следует внимательно изучить.
Gaperton,
> 2) Это определение не конструктивно в том смысле, что не дает прямого способа ("алгоритма") проверить или опровергнуть соответствие ему. > 3) Введение понятий специфицкации и корректности в определение можно избежать. Бритва Оккама.
Боюсь, поворота обсуждения в сторону рассуждений о более точном определении "поведения" избежать будет сложно, т.к., если отталкиваться от твоей трактовки изменения поведения как способности программы определения замены, то многие вполне валидные примеры наследования диагностируемы при замене экземпляра базового класса на унаследованный.
Например:
class Container
{
public:
virtual void insert(Object);
virtual void iterate(Callback);
};
class AssociativeOrderedContainer : public Container
{
. . .
};
очевидно, что ход исполнения программы может различаться в случае ассоциативного упорядоченного контейнера и "произвольного" контейнера, не упорядочивающего элементы, т.к. первый будет всегда итирировать по добавленным объектам в некотором определенном порядке, почти не зависящем от очередности добавления элементов, а второй — скажем, в порядке добавления элементов.
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
Здравствуйте, Павел Кузнецов, Вы писали:
ПК>Gaperton,
>> 2) Это определение не конструктивно в том смысле, что не дает прямого способа ("алгоритма") проверить или опровергнуть соответствие ему. >> 3) Введение понятий специфицкации и корректности в определение можно избежать. Бритва Оккама.
ПК>Боюсь, поворота обсуждения в сторону рассуждений о более точном определении "поведения" избежать будет сложно, т.к., если отталкиваться от твоей трактовки изменения поведения как способности программы определения замены, то многие вполне валидные примеры наследования диагностируемы при замене экземпляра базового класса на унаследованный.
Да, ты совершенно прав. О диагностировании замены говорить нельзя. Либо надо вводить понятие корректности программы, что строго сделать довольно тяжело (особенно если принять во внимание, что в LSP идет речь о любой программе), либо... Придется говорить об инвариантах базового класса, т.е. взять определение подтипа в том виде, в котором он мне изестен из теории. А именно
1) предусловия перекрытых операций не могут быть строже, чем в типе.
2) постусловия перекрытых операций не могут быть слабее, чем в типе.
Для твоего примера:
Контейнер, операция вставки: pred_base = true, post_base = element принадлежит контейнеру;
Сортированый контейнер, вставка:
pred = pred_base (true),
post = post_base (принадлежность контейнеру) && для последовательности вызовов iterate каждый следующий элемент меньше либо равен предыдущему.
Здравствуйте, Павел Кузнецов, Вы писали:
ПК>Gaperton,
>> 2) Это определение не конструктивно в том смысле, что не дает прямого способа ("алгоритма") проверить или опровергнуть соответствие ему. >> 3) Введение понятий специфицкации и корректности в определение можно избежать. Бритва Оккама.
ПК>Боюсь, поворота обсуждения в сторону рассуждений о более точном определении "поведения" избежать будет сложно, т.к., если отталкиваться от твоей трактовки изменения поведения как способности программы определения замены, то многие вполне валидные примеры наследования диагностируемы при замене экземпляра базового класса на унаследованный.
Все нормально, моя трактовка рулит (при небольшом уточнении). Только что разобрался, в чем дело.
Надо ограничить множество программ P оперирующих над Т таким образом, чтобы они полагались на инварианты типа Т. Кстати, мне кажется именно это и имеется в виду в LSP.
Для твоего примера с контейнерами — порядок, в котором добавляются элементы в базовый класс должен быть неопределен. Просто обязан. Если в спецификации базового типа "контейнер" сказано, что они лежат там в том порядке, в котором их туда положили, то твой пример наследования с сортированым контейнером безусловно нарушает LSP. И, кстати, определение подтипа, которое я привел в параллельном посте.
А вот если спецификация не покрывает этот аспект, то, извините, и программа (в т.ч. диагностирующая) на порядок закладываться не должна. Сами понимаете. Именно этими инвариантами и предлагается ограничить класс программ P, из которого предлагается брать диагностирующие тип контрпримеры.
Таким образом, мы все-таки можем уйти от использования понятия "корректности".
Здравствуйте, Павел Кузнецов, Вы писали:
ПК>очевидно, что ход исполнения программы может различаться в случае ассоциативного упорядоченного контейнера и "произвольного" контейнера, не упорядочивающего элементы, т.к. первый будет всегда итирировать по добавленным объектам в некотором определенном порядке, почти не зависящем от очередности добавления элементов, а второй — скажем, в порядке добавления элементов.
Для программы, оперирующей объектами базового типа, поведение объектов подтипа является существенным только когда эта программа знает о существовании подтипов, но в данном случае код нельзя назвать обобщенным. В случае обобщенного кода, поведение подтипов должно быть безразлично, то есть это поведение является черным ящиком. А отличить друг от друга два черных ящика, не заглядывая внутрь их (то есть оставаясь в рамках обобщенного кода) невозможно. А если же ящики недотаточно "черные" (например, дырявые), то и наследование тоже "дырявое"
Gaperton,
> Да, ты совершенно прав. О диагностировании замены говорить нельзя. Либо надо вводить понятие корректности программы, что строго сделать довольно тяжело (особенно если принять во внимание, что в LSP идет речь о любой программе), либо...
Забавно, что работы Барбары Лисков, послужившие поводом для начала разговора, "крутятся" именно вокруг понятия корректности программ. В той же работе (ссылки — ниже), где вводится LSP, речь идет именно о доказуемом поведении программы. Собственно, работа как раз посвящена проблеме того, насколько могут отличаться различные реализации, не влияя на корректность программы. Корректность в данном случае интересна в смысле доказуемости соответствия поведения программы ее спецификации. Наследование — лишь один из рассматриваемых аспектов.
Вот конкретная цитата:
The specification describes what the abstraction does, but omits any information about how it is implemented. By omitting such detail, we permit many different implementations. An implementation is correct if it provides the behavior defined by the specification. Correctness can be proved mathematically if the specification is written in a language with precise semantics; otherwise we establish correctness by informal reasoning or by the somewhat unsatisfactory technique of testing. Correct implementations differ from one another in how they work, i.e., what algorithms they use, and therefore they may have different performance. Any correct implementation is acceptable to the caller provided it meets the caller's performance requirements. Note that correct implementations need not be identical to one another; the whole point is to allow implementations to differ, while ensuring that they remain the same where this is important. The specification describes what is important.
И еще, в качестве иллюстрации, совсем недалеко от формулировки LSP:
First, a set is not a subtype of a list nor is the reverse true. If the same element is added to a set twice, the result is the same as if it had been added only once and the element is counted only once in computing the size of the set. However, if the same element is added twice to a list, it occurs in the list twice. Thus a program expecting a list might not work if passed a set; similarly a program expecting a set might not work if passed a list.
Таким образом, речь идет не совсем о любой программе, а о любой корректной программе, при условии того, что программа основана только на спецификации используемого типа, и не "лезет" в детали его реализации. И под "изменением поведения" в формулировке LSP подразумевается именно то, что замена типа на подтип не должна влиять на корректность программы, т.е. на доказуемость соответствия программы своей спецификации.
> Придется говорить об инвариантах базового класса, т.е. взять определение подтипа в том виде, в котором он мне изестен из теории. > > <...> > > Для твоего примера: > > Контейнер, операция вставки: pred_base = true, post_base = element принадлежит контейнеру; > Сортированый контейнер, вставка: > pred = pred_base (true), > post = post_base (принадлежность контейнеру) && для последовательности вызовов iterate каждый следующий элемент меньше либо равен предыдущему.
В качестве резюме, можно сказать, что в LSP речь идет не о конкретном реализуемом варианте действий, а о множестве допустимых вариантов действий ("поведение") типа T и его подтипа S. А именно: подтип S не должен реализовывать "поведение" (множество реализуемых вариантов действий), выходящее за рамки "поведения" (множества допустимых вариантов действий) типа T. Допустимое поведения типа T задается его спецификацией, включающей:
Инварианты типа, задающие множество допустимых "значений" данного типа (если угодно, множество допустимых состояний его объектов).
Пред- и постусловия всех его методов (собственно, это и есть описание "поведения" в терминах Барбары Лисков), включающие, помимо прочего, и потенциально порождаемые исключения.
Возвращаясь к нашим баранам, т.е. к квадрату и прямоугольнику, если пытаться наследовать квадрат от прямоугольника, то допустимость такого наследования будет определять спецификация "поведения" прямоугольника. В частности, если мутирующих операций в спецификации прямоугольника нет, то такое наследование почти наверняка допустимо.
Также вполне возможна спецификация типа прямоугольника, имеющего мутирующие операции, такая, что одной из вполне валидных его реализаций будет квадрат. Например, если в числе постусловий функции SetWidth перечислена возможность изменения не только высоты, но и ширины. Или если в прямоугольнике есть функция SetDimensions(int width, int height), для которой сказано, что она может порождать исключение, свидетельствующее о недопустимости заданной комбинации значений.
Другой вопрос, насколько осмысленно введение подобной абстракции "прямоугольника", если от него все время нужно ждать какой-нибудь "пакости"...
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
Gaperton,
> Все нормально, моя трактовка рулит (при небольшом уточнении). Только что разобрался, в чем дело. > > Надо ограничить множество программ P оперирующих над Т таким образом, чтобы они полагались на инварианты типа Т. Кстати, мне кажется именно это и имеется в виду в LSP.
Да, именно поэтому я уточнял твое сообщение таким образом:
Полагаю, более практично говорить соответствии программы своей спецификации, при условии, что программа корректна, т.е. учитывает все возможные исходы использования T, заданные его спецификацией. Говоря о поведении, Барбара Лисков как раз говорит о спецификации и соответствии требованиям.
"Полагались на инварианты типа T" — одно из условий, включенных в соответствие спецификации. Где я был не точен, так это в "учитывает все возможные исходы использования T, заданные его спецификацией". Т.е. тут, вроде, все верно, но есть более сильное требование, чем необходимо: намного проще говорить о существовании программы, корректность которой нарушается, при условии, что она учитывает только исходы использования Т, заданные его спецификацией.
.
> Для твоего примера с контейнерами — порядок, в котором добавляются элементы в базовый класс должен быть неопределен. Просто обязан. Если в спецификации базового типа "контейнер" сказано, что они лежат там в том порядке, в котором их туда положили, то твой пример наследования с сортированым контейнером безусловно нарушает LSP. И, кстати, определение подтипа, которое я привел в параллельном посте.
Да, согласен. Это замечание лишний раз подчеркивает то, что в LSP речь идет о соответствии спецификации.
> А вот если спецификация не покрывает этот аспект, то, извините, и программа (в т.ч. диагностирующая) на порядок закладываться не должна. Сами понимаете. Именно этими инвариантами и предлагается ограничить класс программ P, из которого предлагается брать диагностирующие тип контрпримеры. > > Таким образом, мы все-таки можем уйти от использования понятия "корректности".
Не уйдем
Не уйдем, т.к. понятие спецификации вводится именно в ходе попыток доказательства корректности программ, и именно к этой области относятся работы Барбары Лисков. Вне рассуждений о возможности доказательства корректности программы, твоя фраза: "если спецификация не покрывает этот аспект, то, извините, и программа (в т.ч. диагностирующая) на порядок закладываться не должна," — теряет свою силу, т.к. программа должна ограничиваться только информацией о типе, сообщаемой его спецификацией, именно для того, чтобы была возможность доказательства корректности данной программы (т.е. соотвествия ее своей спецификации).
Подробнее см. упомянутое соседнее сообщение.
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
prVovik,
> ПК> очевидно, что ход исполнения программы может различаться в случае ассоциативного упорядоченного контейнера и "произвольного" контейнера, не упорядочивающего элементы, т.к. первый будет всегда итирировать по добавленным объектам в некотором определенном порядке, почти не зависящем от очередности добавления элементов, а второй — скажем, в порядке добавления элементов.
> Для программы, оперирующей объектами базового типа, поведение объектов подтипа является существенным только когда эта программа знает о существовании подтипов, но в данном случае код нельзя назвать обобщенным. <...>
Именно для подведения к необходимости введения понятия спецификации при обсуждении "поведения" в LSP и давался этот пример
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
Здравствуйте, Павел Кузнецов, Вы писали:
ПК>Gaperton,
>> Все нормально, моя трактовка рулит (при небольшом уточнении). Только что разобрался, в чем дело. >> >> Надо ограничить множество программ P оперирующих над Т таким образом, чтобы они полагались на инварианты типа Т. Кстати, мне кажется именно это и имеется в виду в LSP.
ПК>Да, именно поэтому я уточнял твое сообщение таким образом: ПК>
ПК>Полагаю, более практично говорить соответствии программы своей спецификации, при условии, что программа корректна, т.е. учитывает все возможные исходы использования T, заданные его спецификацией. Говоря о поведении, Барбара Лисков как раз говорит о спецификации и соответствии требованиям.
Разница в том, что. Ты говоришь о спецификации программы P, и о корректности P. Я тебя понимаю, и утверждаю, что это сложно, а для наших целей достаточно говорить о спецификации T и о существовании программы p — детектора подтипа, который закладывается только на спецификацию Т. Я утверждаю, что это определение эквивалентно, но проще.
ПК>"Полагались на инварианты типа T" — одно из условий, включенных в соответствие спецификации. Где я был не точен, так это в "учитывает все возможные исходы использования T, заданные его спецификацией". Т.е. тут, вроде, все верно, но есть более сильное требование, чем необходимо: намного проще говорить о существовании программы, корректность которой нарушается, при условии, что она учитывает только исходы использования Т, заданные его спецификацией.
То есть ты согласен, что так как я предлагаю — проще? Мы договорились, или я тебя не понял?
>> Для твоего примера с контейнерами — порядок, в котором добавляются элементы в базовый класс должен быть неопределен. Просто обязан. Если в спецификации базового типа "контейнер" сказано, что они лежат там в том порядке, в котором их туда положили, то твой пример наследования с сортированым контейнером безусловно нарушает LSP. И, кстати, определение подтипа, которое я привел в параллельном посте.
ПК>Да, согласен. Это замечание лишний раз подчеркивает то, что в LSP речь идет о соответствии спецификации.
Еще раз, мы с тобой говорим о разных спецификациях. Ты — о P, я — о T. С чем ты согласен?
>> А вот если спецификация не покрывает этот аспект, то, извините, и программа (в т.ч. диагностирующая) на порядок закладываться не должна. Сами понимаете. Именно этими инвариантами и предлагается ограничить класс программ P, из которого предлагается брать диагностирующие тип контрпримеры. >> >> Таким образом, мы все-таки можем уйти от использования понятия "корректности".
ПК>Не уйдем
ПК>Не уйдем, т.к. понятие спецификации вводится именно в ходе попыток доказательства корректности программ, и именно к этой области относятся работы Барбары Лисков.
Это не важно в контексте нашего разговора, и я все таки предпочел бы от доказательств корректности уйти. Я читал учебный курс за авторством Лисков касательно доказательства корректности, представляю себе что это такое, и считаю это оффтопом. Как мне кажется, можно сформулировать LSP без необходимости привлекать теории доказательства корректности. И эту формулировку я привел — в качестве доказательства.
ПК>Вне рассуждений о возможности доказательства корректности программы, твоя фраза: "если спецификация не покрывает этот аспект, то, извините, и программа (в т.ч. диагностирующая) на порядок закладываться не должна," — теряет свою силу, т.к. программа должна ограничиваться только информацией о типе, сообщаемой его спецификацией, именно для того, чтобы была возможность доказательства корректности данной программы (т.е. соотвествия ее своей спецификации).
Нет, не согласен категорически. Нам нет никакой необходимости доказывать корректность программы P, если мы пользуемся определением LSP в моей формулировке. Если не согласен, объясни пожалуйста — зачем нам этим заниматься.
Gaperton,
> Разница в том, что. Ты говоришь о спецификации программы P, и о корректности P. Я тебя понимаю, и утверждаю, что это сложно, а для наших целей достаточно говорить о спецификации T и о существовании программы p — детектора подтипа, который закладывается только на спецификацию Т. Я утверждаю, что это определение эквивалентно, но проще. > <...> > То есть ты согласен, что так как я предлагаю — проще? Мы договорились, или я тебя не понял?
Согласен. Договорились. Для того, чтобы просто диагностировать нарушение LSP, корректность программы можно оставить за рамками.
> Это не важно в контексте нашего разговора, и я все таки предпочел бы от доказательств корректности уйти. Я читал учебный курс за авторством Лисков касательно доказательства корректности, представляю себе что это такое, и считаю это оффтопом. Как мне кажется, можно сформулировать LSP без необходимости привлекать теории доказательства корректности.
Сформулировать — можно. Только без рассуждении о доказательстве корректности программ не очень понятно, что с LSP делать Впрочем, настаивать не буду: если мы ограничимся самим фактом формулировки LSP, и не будем говорить о том, зачем же мы его формулировали, то да, в формулировку корректность можно не тянуть.
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
Здравствуйте, Павел Кузнецов, Вы писали:
ПК>Сформулировать — можно. Только без рассуждении о доказательстве корректности программ не очень понятно, что с LSP делать Впрочем, настаивать не буду: если мы ограничимся самим фактом формулировки LSP, и не будем говорить о том, зачем же мы его формулировали, то да, в формулировку корректность можно не тянуть.
Почему это не будем. Очень даже будем . Ответ прост — соблюдение LSP уменьшает хрупкость и связность системы. Таким образом, он упрощает ее модификацию, и в long term удешевляет разработку.
Gaperton,
> ПК> Сформулировать — можно. Только без рассуждении о доказательстве корректности программ не очень понятно, что с LSP делать Впрочем, настаивать не буду: если мы ограничимся самим фактом формулировки LSP, и не будем говорить о том, зачем же мы его формулировали, то да, в формулировку корректность можно не тянуть.
> Почему это не будем. Очень даже будем . Ответ прост — соблюдение LSP уменьшает хрупкость и связность системы. Таким образом, он упрощает ее модификацию, и в long term удешевляет разработку.
Логично Вопрос — как достигается эта магия?
Имхо, благодаря тому, что LSP вносит свой вклад в очерчивание пределов допустимых вариаций в реализациях абстракций, не влияющих на корректность программ (соответствие их своей спецификации), использующих данные абстракции (на основе их спецификаций).
А именно: при нарушении LSP (т.е. при создании наследников, не соответствующих спецификации базового класса) может произойти нарушение соответствия спецификации программ, использующих базовые классы (на основе их спецификации); при соблюдении LSP могут "сломаться" только те программы, которые были основаны на какой-то дополнительной информации, за пределами спецификации поведения базовых классов (*). Соответственно, без следования LSP, для того, чтобы удостовериться в корректности программы после модификации наследника (или, что то же самое, введении нового наследника), нужно будет проанализировать все места, где используются базовые типы. При соблюдении LSP такой анализ для доказуемо корректных программ проводить не нужно (**). Последнее и есть уменьшение хрупкости (т.е. в нарушении корректности при модификациях) и связности (тут я не уверен в точности русского термина, но, совершенно очевидно, что ты говорил о coupling, а не cohesion, т.к. последнее — "положительная" метрика).
Грубо говоря, LSP — один из принципов, позволяющих разделить ответственность за корректность работы программ: если был введен наследник, не соответствущий спецификации базового класса, "виноват" автор класса-наследника (или базового класса, неточно составивший спецификацию); если наследник соответствует LSP, но использующая базовый класс программа "сломалась" — "виноват" автор этой программы.
Собственно, я мог воздержаться от пространных рассуждений, т.к. использование тобой слова "хрупкость", имхо, фактически, автоматом приводит к понятию корректности.
(*) Трюизм, а сколько копий вокруг прямоугольников и квадратов ломается
(**) Вот куда я, действительно, не хочу сейчас идти, так это в дебри практического использования доказательств корректности программ, но, к сожалению, упомянуть приходится.
Posted via RSDN NNTP Server 2.0 beta
Легче одурачить людей, чем убедить их в том, что они одурачены. — Марк Твен
Здравствуйте, Gaperton, Вы писали:
G>Программа определена в терминах Т. Ее поведение не должно измениться именно в этих терминах. Это действительно немного путанный момент — можно мне переформулировать так, чтобы было понятнее? G>
G>Если для любого o1 <- S найдется такой o2 <- T, что не будет существовать такой программы p, которая при замене o1 на o2 способна определить эту замену, то S является подтипом T.
По поводу такой формуллировки у Вас развернулась замечательная дискуссия с Павлом Кузнецовым.
G>Насчет "определить замену" — на случай, если вы опять не поймете, поясню. Это означает, что вы не сможете написать программу, которая, пользуясь интерфейсом Т, могла бы понять, что ей подпихнули подтип этого Т — S.
Это — ошибка. Смысл-то как раз в том, что P не должна, как Вы выразились, "понять" что ей "подпихнули" S вместо T.
G>Или, что то же самое, подтип не должен нарушать инвариантов типа.
Вот с этим полностью согласен. Необходимое условие behavioural subtyping:
Если всё множество инвариантов типа T, является подмножеством инвариантов типа S, то S — подтип T.
Выполнение этого условия означает теоритическую возможность реализации типом S всего поведения типа T... + something extra. И дает подвод для subclassing'га. Возвращаясь к квадрату и прямоугольнику: все множество инвариантов квадрата лежит внутри множества инвариантов прямоугольника.
Дело за малым — сформулировать условие достаточности . Это нужно, т.к. данное определение не учитывает т.н. state chain предикатов... констрайнов. В том, смысле, что вполне может оказаться что из некоторого множества инвариантов T (B)- не пересекающегося с множеством инвариантов S (A) — невозможно перейти к инварианту из A{}.
Для пары квадрат/прямоугольник верно утверждение, что из любого инварианта из B{} мы можем перейти к инварианту из A{}.
G>В контексте этого разговора довольно забавно выглядят ваши слова. G>
G>И лучше бы перед тем как... почитать таки оригинал. Это поможет снять некоторые вопросы. И может быть Вам после этого станет ясно, почему, например, уже в определении ПЛВ нет этих терминов.
Угу... Потому что если бы Вы таки прочли хотябы тот абзац из которого "выдернуто" определение ППЛ, то, смею надеятся, что Вы бы поняли что речь идёт не более чем о:
The intuitive idea of a subtype is one whose objects provide all the behavior of objects of another type (the supertype) plus something extra.
Что в последствии и было сформулировано в досточном условии... в котором нет таких терминов как: программа, неизменно и т.п.
G>>> Ну да ладно, давайте сюда ваше определение "behavioral subtyping". И давайте посмотрим, каким образом оно сделает вашу ошибку правильным решением.
G>> Для начала указали бы мне на "ошибку"... а то я, по глупости своей, её так и не увидел.
Люди, знакомые с определением, его там увидели, несмотря на то, что я назвал это "наследованием". Ниже по ветке вы можете видеть дискуссию с Олегом на эту тему. Это, кстати, совершенно неважно, разговор не об этом.
Ещё раз... Сама Лисков не считает сформуллированный ей же принцип подстановки каким-либо условием определяющим наличие behavioural subtyping. Это-то Вам надеюсь понятно?
G>Впрочем, я разговор заканчиваю, надоело смертельно.
Здравствуйте, Gaperton, Вы писали:
G>Разница в том, что. Ты говоришь о спецификации программы P, и о корректности P. Я тебя понимаю, и утверждаю, что это сложно, а для наших целей достаточно говорить о спецификации T и о существовании программы p — детектора подтипа, который закладывается только на спецификацию Т. Я утверждаю, что это определение эквивалентно, но проще.
+1. Наконец-то!!! Вот это:
достаточно говорить о спецификации T и о существовании программы p — детектора подтипа, который закладывается только на спецификацию Т.
прктически, эквивалентно:
Let phi(x) be a property provable about objects x of type T. Then phi(y) should be true for objects y of type S where S is a subtype of T.
Осталось разубедить Вас в том, что нет необходимости рассматривать всё возможное множество phi.
Здравствуйте, prVovik, Вы писали:
V>Для программы, оперирующей объектами базового типа, поведение объектов подтипа является существенным только когда эта программа знает о существовании подтипов, но в данном случае код нельзя назвать обобщенным. В случае обобщенного кода, поведение подтипов должно быть безразлично, то есть это поведение является черным ящиком. А отличить друг от друга два черных ящика, не заглядывая внутрь их (то есть оставаясь в рамках обобщенного кода) невозможно. А если же ящики недотаточно "черные" (например, дырявые), то и наследование тоже "дырявое"
+1. Дружно медитируем над двумя "черными" ящиками...
class S
{
private int _size;
public int Size
{
get{return _size;}
set{_size = value;}
}
public int Area
{
get{return (_size * _size);}
}
}
class R: S
{
private int _width;
public int Height
{
get{return base.Size;}
set{base.Size = value;}
}
public int Width
{
get{return _width;}
set{_width = value;}
}
new public int Area
{
get{return (base.Size * _width);}
}
}
Здравствуйте, AndrewVK, Вы писали:
AVK>Здравствуйте, gbear, Вы писали:
G>>Тем не менее, для реализации вписаной окружности достаточно реализовать в прямоугольнике привидение его к "квадратному" виду. Т.е. если мы обращаетмся к R.GetInscribedCircle() то R.Width становится равно S.Size.
AVK>Т.е. делаем функционал, который в постановке задачи отсутствовал. Это называется архитектурной ошибкой.
1. Наличие Inscribed Circle у прямоугольника возможно только в четко определенном его инварианте. Соответсвенно, если агрегат требует наличия Inscribed Circle (а он именно требует, т.к. работает с прямоугольником через контракт квадрата) нам нужно привести прямоугольник к этому инварианту.
A>>>В результате получаем семантически непонятный результат. Еще хуже.
G>>Можно по подробней... о том, что Вы понимаете под "семантически непонятный"?
AVK>В том, что смысл того функционала, о котором я говорил, применительно к пямоугольнику неясен.
А, он и не должен быть ясен применительно к прямоугольнику Его применяют к квадрату.
Здравствуйте, Павел Кузнецов, Вы писали:
ПК>Можно говорить не об изменении существущих экземпляров, а о создании новых. ПК>Так, например, происходит в случае "чистого" функционального программирования, ПК>которое в этом смысле как раз достаточно близко к математике.
Ну, хорошо, пусть о создании новых. А что это меняет в моем рассуждении? Просто вместо операции изменения есть операция создания. И тогда она уже не может быть полиморфна для прямоугольников и квадратов. Именно с точки зрения математики.
и это пункт 3.
. Это нужно, т.к. данное определение не учитывает т.н. state chain предикатов... констрайнов. В том, смысле, что вполне может оказаться что из некоторого множества инвариантов T (B)- не пересекающегося с множеством инвариантов S (A) — невозможно перейти к инварианту из A{}.
Для начала указали бы мне на "ошибку"... а то я, по глупости своей, её так и не увидел. 
