DG>>>это лишь означает, что: DG>>>1. во-первых, для данного программы можно определить как хочется DG>>>2. во-вторых, что для данной программы такое построение делать не стоит, но из этого не следует, что его не стоит делать для произвольной программы S>>Это означает что твоя идентичность не позволяет отличать объекты.
DG>да, для "плохих" программ не позволяет. зато позволяет в хороших
А ООП идентичность работает для всех программ.
DG>>>ссылка же это зависимое (производное) понятие от объекта, потому оно меняется при переходе, если переопределяется понятие объекта. DG>>>как именно меняется зависит от того, как оно определено в рамках данной теории. S>>То есть ты не знаешь, но термином пользуешься.
DG>я встречал штук 20 определений понятия ссылка (часть из них хорошая, часть не очень). DG>но на текущий момент, именно ты узурпировал право решать — определения какого авторитета считать правильным. DG>поэтому я жду, когда ты примешь решение какое определение ссылки ты считаешь правильным.
Хорошо, предлагай. Со ссылкой на авторитета. А я буду решать
DG>>да, для "плохих" программ не позволяет. зато позволяет в хороших S>А ООП идентичность работает для всех программ.
не для всех, как уже выше разбирали — например, ecma-идентичность не во всех случаях является ООП-идентичность
во-вторых, при конструктивном подходе недоопределенность или противоречия сами по себе не мешают, потому что в большинстве случаев можно сделать доопределение.
например, для .net-а можно взять функцию идентичности (и доопределить ее на основе ecma-identity):
если оба double.IsNan — true
если оба value-type (в том числе и забоксированный) — equals
если оба строка — equals
иначе (оба ссылочный-тип или оба разных видов) — referenceequals
для твоего контрпримера достаточно мою функцию идентичности доопределить как: если трассу не получилось установить, то объекты различные.
это приводит к главному вопросу:
если в одной программе можно построить несколько функций идентичности, то какую лучше выбрать?
и ответ ту которая более полиморфная: с большим кол-ва кода позволяет работать один и тем же образом.
если есть функция идентичности, которая позволяет единым образом обрабатывать изменения immutable-объекта и изменения mutable-объекта, то стоит выбирать именно такую функцию идентичности.
DG>>я встречал штук 20 определений понятия ссылка (часть из них хорошая, часть не очень). DG>>но на текущий момент, именно ты узурпировал право решать — определения какого авторитета считать правильным. DG>>поэтому я жду, когда ты примешь решение какое определение ссылки ты считаешь правильным. S>Хорошо, предлагай. Со ссылкой на авторитета. А я буду решать
ссылка — аксиоматическое (или другими словами неопределяемое через более элементарные понятия) понятие.
описание (оно же свойства):
элемент, посредством которого осуществляется работа с объектом (через ссылку посылаются сообщения реальному объекту).
ссылка — объект в границах локальной системы, через который посылаются сообщения объекту во внешней системе.
обычно ссылка не отчуждаема от текущего контекста (и этим отличается от идентификатора)
пример 1:
возьмем в качестве локальной системы — функцию.
внутри границ такой системы находится только stack-frame (переменные-параметры и локальные переменные).
heap — это внешняя система. и для того, чтобы работать с объектами из внешней системы в переменную помещается ссылка.
пример 2:
локальная система — .net app domain.
объект-RealProxy — есть ссылка на объект из внешней системы.
пример 3:
локальная система — компьютер пользователя
пользовательский интерфейс www.rsdn.ru загруженный в браузер — есть ссылка на объект БД rsdn.ru
DG>>>да, для "плохих" программ не позволяет. зато позволяет в хороших S>>А ООП идентичность работает для всех программ.
DG>не для всех, как уже выше разбирали — например, ecma-идентичность не во всех случаях является ООП-идентичность
В каких не является? Где я был?
DG>во-вторых, при конструктивном подходе недоопределенность или противоречия сами по себе не мешают, потому что в большинстве случаев можно сделать доопределение.
Я бы это назвал "немного ослабить". DG>например, для .net-а можно взять функцию идентичности (и доопределить ее на основе ecma-identity): DG>если оба double.IsNan — true
Обалдеть. А ничего что там могут быть PositiveInfinity и NegativeInfinity?
DG>если оба value-type (в том числе и забоксированный) — equals
Equals от ValueType не годится для идентичности, т.к. позволяет быть идентичными объектам с разными состояниями. DG>если оба строка — equals
То же самое. DG>иначе (оба ссылочный-тип или оба разных видов) — referenceequals
DG>для твоего контрпримера достаточно мою функцию идентичности доопределить как: если трассу не получилось установить, то объекты различные.
В моем контрпримере трассу установить удалось. В частности, "" и "1" входят в одну трассу. Но ты утверждаешь что их идентичность неопределена.
DG>это приводит к главному вопросу: DG>если в одной программе можно построить несколько функций идентичности, то какую лучше выбрать?
Ты сейчас задаешь вопрос уровня "если в одном поле можно построить несколько аддитивных функций, то какую лучше выбрать?"
DG>и ответ ту которая более полиморфная: с большим кол-ва кода позволяет работать один и тем же образом. DG>если есть функция идентичности, которая позволяет единым образом обрабатывать изменения immutable-объекта и изменения mutable-объекта, то стоит выбирать именно такую функцию идентичности.
Именно такая и выбрана в ecma.
DG>>>поэтому я жду, когда ты примешь решение какое определение ссылки ты считаешь правильным. S>>Хорошо, предлагай. Со ссылкой на авторитета. А я буду решать
DG>ссылка — аксиоматическое (или другими словами неопределяемое через более элементарные понятия) понятие. DG>описание (оно же свойства): DG>элемент, посредством которого осуществляется работа с объектом (через ссылку посылаются сообщения реальному объекту).
Не конкретно. Что за элемент? XML? Контроллер памяти? Источник не указан.
DG>ссылка — объект в границах локальной системы, через который посылаются сообщения объекту во внешней системе. DG>обычно ссылка не отчуждаема от текущего контекста (и этим отличается от идентификатора)
DG>пример 1: DG>возьмем в качестве локальной системы — функцию. DG>внутри границ такой системы находится только stack-frame (переменные-параметры и локальные переменные). DG>heap — это внешняя система. и для того, чтобы работать с объектами из внешней системы в переменную помещается ссылка.
DG>пример 2: DG>локальная система — .net app domain. DG>объект-RealProxy — есть ссылка на объект из внешней системы.
DG>пример 3: DG>локальная система — компьютер пользователя DG>пользовательский интерфейс www.rsdn.ru загруженный в браузер — есть ссылка на объект БД rsdn.ru
DG>данное определение предложено DarkGray-ем
DarkGray для меня не авторитет в области выдумывания определений. К тому же определение ссылки основано на определении объекта, с идентичностью которого в определениях DG я наблюдаю серьезные несоответствия с OOP. Кроме того, какие-то системы, контексты, локальности.
На правах, данными мне через узурпирование мной прав решать о правильности определений, говорю — не годится.
DG>>во-вторых, при конструктивном подходе недоопределенность или противоречия сами по себе не мешают, потому что в большинстве случаев можно сделать доопределение. S>Я бы это назвал "немного ослабить". DG>>например, для .net-а можно взять функцию идентичности (и доопределить ее на основе ecma-identity): DG>>если оба double.IsNan — true S>Обалдеть. А ничего что там могут быть PositiveInfinity и NegativeInfinity?
чё? там быть — это где? и чему это мешает?
научись все-таки грамотно формулировать свои сомнения. хотя бы в виде: если принять это допущение, и потом сделать вот так и вот так, то будет жопа.
DG>>если оба value-type (в том числе и забоксированный) — equals S>Equals от ValueType не годится для идентичности, т.к. позволяет быть идентичными объектам с разными состояниями.
в каких сообщений это проявляется?
DG>>это приводит к главному вопросу: DG>>если в одной программе можно построить несколько функций идентичности, то какую лучше выбрать? S>Ты сейчас задаешь вопрос уровня "если в одном поле можно построить несколько аддитивных функций, то какую лучше выбрать?"
выбор аддитивной функции определяет поле в котором происходит работа.
так, например, в булевой логике — аддитивную функцию можно взять хor и будет одно поле, а можно взять == и будет другое поле.
тоже самое и с ооп, для одного и того же кода, можно взять разные функции идентичности, и будет разные ООП с разным делением
DG>>ссылка — аксиоматическое (или другими словами неопределяемое через более элементарные понятия) понятие. DG>>описание (оно же свойства): DG>>элемент, посредством которого осуществляется работа с объектом (через ссылку посылаются сообщения реальному объекту). S>Не конкретно. Что за элемент? XML? Контроллер памяти? Источник не указан.
неопределяемые понятия и не бывают конкретными. пойди посмотри определение точки или множества и найди там конкретность
вот где здесь конкретность?:
В современной аксиоматике геометрии точка является первичным понятием, задаваемым перечнем его свойств.
элемент — это то, что выделили из пространства. некий отдельный рассматриваемый "атом" "пространства".
S>DarkGray для меня не авторитет в области выдумывания определений.
вот именно поэтому в математике и не используют авторитеты, никто же не говорит, что понятие поле правильное потому что его предложил Евклид, Абель или кто-то еще.
в математике (как и в любой точной науке) — правильность определения проверяется лишь по соотношению двух критериев: насколько много из определения можно выводов сделать, и к скольки ситуациям определение можно применить.
Здравствуйте, DarkGray, Вы писали:
DG>>>во-вторых, при конструктивном подходе недоопределенность или противоречия сами по себе не мешают, потому что в большинстве случаев можно сделать доопределение. S>>Я бы это назвал "немного ослабить". DG>>>например, для .net-а можно взять функцию идентичности (и доопределить ее на основе ecma-identity): DG>>>если оба double.IsNan — true S>>Обалдеть. А ничего что там могут быть PositiveInfinity и NegativeInfinity?
DG>чё? там быть — это где? и чему это мешает? DG>научись все-таки грамотно формулировать свои сомнения. хотя бы в виде: если принять это допущение, и потом сделать вот так и вот так, то будет жопа.
Если принять допущение что все double, которые IsNan являются одним объектом, то выходит что ответ на сообщения IsPositive(Negative)Infinity неопределен. Ты мог бы определить одним объектом все даблы < 1.0 с тем же успехом. Да, я помню, для тебя это совершенно не жопа, ты даже пытался определить идентичными даблы, разница которых по модулю меньше епсилон.
DG>>>если оба value-type (в том числе и забоксированный) — equals S>>Equals от ValueType не годится для идентичности, т.к. позволяет быть идентичными объектам с разными состояниями.
DG>в каких сообщений это проявляется?
В каких-нибудь. Например, может проявиться в сообщениях ToString.
DG>>>это приводит к главному вопросу: DG>>>если в одной программе можно построить несколько функций идентичности, то какую лучше выбрать? S>>Ты сейчас задаешь вопрос уровня "если в одном поле можно построить несколько аддитивных функций, то какую лучше выбрать?"
DG>выбор аддитивной функции определяет поле в котором происходит работа. DG>так, например, в булевой логике — аддитивную функцию можно взять хor и будет одно поле, а можно взять == и будет другое поле. DG>тоже самое и с ооп, для одного и того же кода, можно взять разные функции идентичности, и будет разные ООП с разным делением
Да. Но проблемма твоего ООП в том, что твое деление не удовлетворяет идентичности ООП.
DG>>>ссылка — аксиоматическое (или другими словами неопределяемое через более элементарные понятия) понятие. DG>>>описание (оно же свойства): DG>>>элемент, посредством которого осуществляется работа с объектом (через ссылку посылаются сообщения реальному объекту). S>>Не конкретно. Что за элемент? XML? Контроллер памяти? Источник не указан.
DG>неопределяемые понятия и не бывают конкретными. пойди посмотри определение точки или множества и найди там конкретность DG>вот где здесь конкретность?: DG>
DG>В современной аксиоматике геометрии точка является первичным понятием, задаваемым перечнем его свойств.
DG>элемент — это то, что выделили из пространства. некий отдельный рассматриваемый "атом" "пространства".
Я вижу твои определения закручены в кольцо. Идентичность объкта ты определяешь через ссылку, сыслку через объект, атом, пространство и т.п. Что же у тебя все-таки аксиоматичнее? ссылка или объект?
S>>DarkGray для меня не авторитет в области выдумывания определений.
DG>вот именно поэтому в математике и не используют авторитеты, никто же не говорит, что понятие поле правильное потому что его предложил Евклид, Абель или кто-то еще. DG>в математике (как и в любой точной науке) — правильность определения проверяется лишь по соотношению двух критериев: насколько много из определения можно выводов сделать, и к скольки ситуациям определение можно применить.
Я пока не увидел ни одного полезного вывода из твоих определений. И ни одной ситуации, в которой они были бы полезнее, чем ООП аналоги.
Докажи сначала право твоих определений на существование в рамках ООП, т.е. непротиворечивость им.
Начни с того, какой смысл в существовании объекта, который отвечает на сообщения неопределенным образом. Примеры — строки с твоей идентичностью, где объект на сообщение Length может вернуть что угодно... Double с IsPositiveInfinity...
S>Я вижу твои определения закручены в кольцо. Идентичность объкта ты определяешь через ссылку, сыслку через объект, атом, пространство и т.п. Что же у тебя все-таки аксиоматичнее? ссылка или объект?
они оба аксиоматичны.
не путай три различные вещи: определение, способ конструирования и описание. они внешне похожи, но ничего общего между собой не имеют.
вопрос на засыпку — сколько неопределяемых понятий и аксиом в евклидовой геометрии?
в ООП как минимум есть следующие неопределяемые понятия:
объект
состояние
поведение
ссылка
сообщение
отправка/получение сообщения
кстати, в ООП неявно подразумевается, что сообщение объекту может отправляться только через ссылку.
и именно через это объясняется, почему функция F1 может послать сообщение объекту z, а у функции F2 нет способа отправить сообщение объекту z
void F1(Z z)
{
z.SendMessage();
}
void F2()
{
}
void Main()
{
var z= new Z();
F1(z);
F2();
}
S>Докажи сначала право твоих определений на существование в рамках ООП, т.е. непротиворечивость им.
для начала приведи, что чему не должно противоречить.
пока ты не привел вообще ни одного формализованного требования.
S>Начни с того, какой смысл в существовании объекта, который отвечает на сообщения неопределенным образом. Примеры — строки с твоей идентичностью, где объект на сообщение Length может вернуть что угодно...
такого противоречия нет — при одновременном использовании трасс и понятия версионного объекта
S> Double с IsPositiveInfinity...
Здравствуйте, DarkGray, Вы писали:
S>>Я вижу твои определения закручены в кольцо. Идентичность объкта ты определяешь через ссылку, сыслку через объект, атом, пространство и т.п. Что же у тебя все-таки аксиоматичнее? ссылка или объект?
DG>они оба аксиоматичны.
DG>не путай три различные вещи: определение, способ конструирования и описание. они внешне похожи, но ничего общего между собой не имеют.
Ок, не буду
DG>вопрос на засыпку — сколько неопределяемых понятий и аксиом в евклидовой геометрии?
Считай, что засыпался. Я этим вопросом не занимался. Но имею мнение. Евклид описывал понятия. Аналитическая геометрия их определяет на основе теории множеств. Аксиом 5 штук.
DG>в ООП как минимум есть следующие неопределяемые понятия: DG>объект DG>состояние DG>поведение DG>ссылка DG>сообщение DG>отправка/получение сообщения
У меня такое ощущение, что все на что ты хотел начихать, ты засунул в неопределяемые понятия.
DG>кстати, в ООП неявно подразумевается, что сообщение объекту может отправляться только через ссылку.
В ООП очень много что неявно подразумевается, на что ты забил. Например, то что объект сохраняет идентичность на все время своего существования. А что только через ссылку — это ты придумал.
DG>и именно через это объясняется, почему функция F1 может послать сообщение объекту z, а у функции F2 нет способа отправить сообщение объекту z DG>
Имеешь право объяснять именно "через это". Мое право — неудовлетворяться таким объяснением.
S>>Докажи сначала право твоих определений на существование в рамках ООП, т.е. непротиворечивость им.
DG>для начала приведи, что чему не должно противоречить. DG>пока ты не привел вообще ни одного формализованного требования.
Приводил.
S>>Начни с того, какой смысл в существовании объекта, который отвечает на сообщения неопределенным образом. Примеры — строки с твоей идентичностью, где объект на сообщение Length может вернуть что угодно...
DG>такого противоречия нет — при одновременном использовании трасс и понятия версионного объекта
То что ты это отрицаешь не исчерпывает противоречия.
S>> Double с IsPositiveInfinity...
DG>тут тем более проблемы нет.
Есть.
Здравствуйте, DarkGray, Вы писали:
DG>не для всех, как уже выше разбирали — например, ecma-идентичность не во всех случаях является ООП-идентичность DG>во-вторых, при конструктивном подходе недоопределенность или противоречия сами по себе не мешают, потому что в большинстве случаев можно сделать доопределение. DG>например, для .net-а можно взять функцию идентичности (и доопределить ее на основе ecma-identity): DG>если оба double.IsNan — true DG>если оба value-type (в том числе и забоксированный) — equals DG>если оба строка — equals DG>иначе (оба ссылочный-тип или оба разных видов) — referenceequals
Отлично. Я надеюсь, вы понимаете, что расширили модель ООП, введя в неё помимо объектов ещё и "экземпляры значимых типов", которые ведут себя по другому?
Само ООП в вашем расширении совершенно не нуждается, и прекрасно работает без него. С возможностью расширять модель ООП никто не спорил с самого начала. Вы пытались доказать, что можно получить ООП, ослабив требования к одной из составляющих модели. Увы.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, DarkGray, Вы писали:
S>>Я вижу твои определения закручены в кольцо. Идентичность объкта ты определяешь через ссылку, сыслку через объект, атом, пространство и т.п. Что же у тебя все-таки аксиоматичнее? ссылка или объект?
DG>они оба аксиоматичны.
DG>не путай три различные вещи: определение, способ конструирования и описание. они внешне похожи, но ничего общего между собой не имеют.
DG>вопрос на засыпку — сколько неопределяемых понятий и аксиом в евклидовой геометрии?
DG>в ООП как минимум есть следующие неопределяемые понятия: DG>объект DG>состояние DG>поведение DG>ссылка DG>сообщение DG>отправка/получение сообщения
Неа. Почти всё определяемо.
Ссылка — это математическое понятие с определённым "математическим поведением". То есть для ссылки определены операции
— сравнения ссылок (вводящая отношение эквивалентности ссылок)
— снятия ссылки (возможность отправить сообщение объекту по ссылке)
объект — это математическое понятие с определённым математическим поведением. В частности, есть понятие "поведение", которое определяется набором всех возможных реакций на все возможные сообщения.
сообщение — это элемент множества возможных сообщений. Способов строить множество сообщений — много. Однако от сообщений требуется только различимость (она нужна для того, чтобы можно было описывать поведение).
состояние объекта — это возможность для него по-разному реагировать на одинаковые сообщения. В полностью детерминистической модели состояние объекта однозначно определяется предысторией отправленных ему сообщений.
И так далее.
DG>кстати, в ООП неявно подразумевается, что сообщение объекту может отправляться только через ссылку.
Да.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
S>Ссылка — это математическое понятие с определённым "математическим поведением". То есть для ссылки определены операции S>- сравнения ссылок (вводящая отношение эквивалентности ссылок) S>- снятия ссылки (возможность отправить сообщение объекту по ссылке)
это зафиксированы свойства — это не означает, что при этом однозначно определено, что такое ссылка.
так же как фиксируется, что у точки нет размерности, но это не означает, что понятие точки определено.
S>объект — это математическое понятие с определённым математическим поведением. В частности, есть понятие "поведение", которое определяется набором всех возможных реакций на все возможные сообщения. S>сообщение — это элемент множества возможных сообщений. Способов строить множество сообщений — много. Однако от сообщений требуется только различимость (она нужна для того, чтобы можно было описывать поведение). S>состояние объекта — это возможность для него по-разному реагировать на одинаковые сообщения. В полностью детерминистической модели состояние объекта однозначно определяется предысторией отправленных ему сообщений.
так можно определять, но здесь появилось новое понятие "реакция на сообщение".
так же есть множества всяких нюансов — следующее поведение одинаковое или нет?
Здравствуйте, DarkGray, Вы писали: DG>это зафиксированы свойства — это не означает, что при этом однозначно определено, что такое ссылка.
Ссылка — это то, что удовлетворяет этим свойствам. Не очень понятно, что вы называете термином "однозначно". Вот что такое рациональные числа — определено однозначно или неоднозначно? Ссылки определены не хуже рациональных чисел.
DG>так можно определять, но здесь появилось новое понятие "реакция на сообщение".
Оно не является атомарным, а определяется в терминах существующих. Реакцией на сообщение является отправка от 0 до N сообщений другим объектам.
DG>так же есть множества всяких нюансов — следующее поведение одинаковое или нет? DG>?
Не очень понятно, что означают ваши формулы, но судя по всему — нет, не одинаковое.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
DG>>это зафиксированы свойства — это не означает, что при этом однозначно определено, что такое ссылка. S>Ссылка — это то, что удовлетворяет этим свойствам. Не очень понятно, что вы называете термином "однозначно". Вот что такое рациональные числа — определено однозначно или неоднозначно? Ссылки определены не хуже рациональных чисел.
рациональное число задано в формате "<существительное> + <свойства>": рациональное число — это число, которое удовлетворяет свойству: представляемое несократимой обыкновенной дробью.
или другими словами — берется элемент известного множества "число", и на него накладываются ограничения.
из какого множества берется "ссылка"? можно ли ссылки брать из множества "объект"?, сейчас определение про это ничего не говорит
DG>>так можно определять, но здесь появилось новое понятие "реакция на сообщение". S>Оно не является атомарным, а определяется в терминах существующих. Реакцией на сообщение является отправка от 0 до N сообщений другим объектам.
из этого определения вытекает, что в понятие "поведение" не входит изменение состояния.
это так и есть? или это ты просто забыл указать?
S> сообщение — это элемент множества возможных сообщений. Способов строить множество сообщений — много
как соотносятся множества сообщений и объектов? пересекаются? одно входит в другое? строго не пересекающиеся? имеют общие вырожденные точки?
как соотносятся между собой множества ссылки и объекты? множества ссылки и сообщения?
на все эти вопросы необходимо ответить, если речь идет о математических определениях
S>Если принять допущение что все double, которые IsNan являются одним объектом, то выходит что ответ на сообщения IsPositive(Negative)Infinity неопределен. Ты мог бы определить одним объектом все даблы < 1.0 с тем же успехом.
вижу, в этой фразе хвост не стыкуется с началом, т.к. double.IsNan(double.NegativeInfinity) возвращает false
Здравствуйте, DarkGray, Вы писали:
S>>Если принять допущение что все double, которые IsNan являются одним объектом, то выходит что ответ на сообщения IsPositive(Negative)Infinity неопределен. Ты мог бы определить одним объектом все даблы < 1.0 с тем же успехом.
DG>вижу, в этой фразе хвост не стыкуется с началом, т.к. double.IsNan(double.NegativeInfinity) возвращает false
Действительно. Я думал, что он вернет true. Лопух.
Но проблема не снимается, т.к. для такого дабла, который (Double.IsNan(x) == true), а он один по определению идентичности DG, существует примерно 2^52-1 вариантов ответа BitConverter.DoubleToInt64Bits(x).
S>Но проблема не снимается, т.к. для такого дабла, который (Double.IsNan(x) == true), а он один по определению идентичности DG, существует примерно 2^52-1 вариантов ответа BitConverter.DoubleToInt64Bits(x).
дальше есть несколько вариантов:
1. если эта функция в программе не используется, то пофигу что она там возвращает.
2. если используется и можно считать, что функция BitConverter.DoubleToInt64Bits — частично случайная: для double.IsNan — она случайно выбирает битовое представление из определенного множества.
и программе такого предположения достаточно, то тоже нет проблемы
это все необходимо для уменьшения кол-ва рассматриваемых вариантов поведения программы, что упрощает задачу доказательства корректности программы
S>>Но проблема не снимается, т.к. для такого дабла, который (Double.IsNan(x) == true), а он один по определению идентичности DG, существует примерно 2^52-1 вариантов ответа BitConverter.DoubleToInt64Bits(x).
DG>дальше есть несколько вариантов: DG>1. если эта функция в программе не используется, то пофигу что она там возвращает. DG>2. если используется и можно считать, что функция BitConverter.DoubleToInt64Bits — частично случайная: для double.IsNan — она случайно выбирает битовое представление из определенного множества. DG>и программе такого предположения достаточно, то тоже нет проблемы
DG>это все необходимо для уменьшения кол-ва рассматриваемых вариантов поведения программы, что упрощает задачу доказательства корректности программы
Что бы уменьшить кол-во рассматриваемых вариантов поведения программы достаточно оперировать эквивалентностью Double.IsNan на определенном множестве операций без подмены идентичности.
И уж точно перевод DoubleToInt64Bits из разряда детерминированных не упростит доказательство корректности там где она используется.
S>Что бы уменьшить кол-во рассматриваемых вариантов поведения программы достаточно оперировать эквивалентностью Double.IsNan на определенном множестве операций без подмены идентичности.
Здравствуйте, DarkGray, Вы писали:
S>>Что бы уменьшить кол-во рассматриваемых вариантов поведения программы достаточно оперировать эквивалентностью Double.IsNan на определенном множестве операций без подмены идентичности.
DG>покажи как используется эквивалентность при доказательстве корректности(или некорректности) следующего кода: DG>http://www.rsdn.ru/forum/philosophy/4553822.aspx?tree=tree
Вообще-то я не подписывался анализировать корректность-некорректность императивного кода. Но для того что бы показать некорректность этого, достаточно его рассахарить. Тогда будет видно что построенные функции умножают не соответствующее значение из последовательности на себя, а умножают на себя значение, равное последнему элементу последовательности.
Для доказательства того что это значение совпадает с последним значением последовательности не нужна эквивалентность по IsNan.
Здравствуйте, DarkGray, Вы писали:
S>>Для доказательства того что это значение совпадает с последним значением последовательности не нужна эквивалентность по IsNan.
DG>где формальное доказательство?
Я же написал, что не подписывался делать формальные доказательства императивного кода. Но направление вот:
class X { public double x; }
X x = new X();
for (var tmp in seq)
x.x = tmp;
Если ты не можешь доказать что при непустом seq в x будет лежать последнее значение из seq после выполнения цикла без того что бы испортить идентичность — то это не мои проблемы.
Что конкретно тебя смущает? Присваивание?
