Программист постоянно делает баги. Это считается нормальным.
Причем не только баги-описки, но баги в самой логике работы программы.
Зачастую оказывается, что используемая модель некорректна даже в теории, при этом на практике она может даже более-менее успешно работать за счет каких-нибудь хакерских методов.

А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?

Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.

1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель, в противном случае количество вариантов будет слишком большим для такого анализа. Например, нужен анализ всех вариантов одновременных операций при доступе нескольких пользователей к иерархии ресурсов.

Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...

*Под абстракцией понимается выделение существенного.

Здравствуйте, HrorH, Вы писали:


HH> Программист постоянно делает баги. Это считается нормальным.
HH> Причем не только баги-описки, но баги в самой логике работы программы.
HH> Зачастую оказывается, что используемая модель некорректна даже в теории, при этом на практике она может даже более-менее успешно работать за счет каких-нибудь хакерских методов.

HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.

HH> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
HH> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
HH> 3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель, в противном случае количество вариантов будет слишком большим для такого анализа. Например, нужен анализ всех вариантов одновременных операций при доступе нескольких пользователей к иерархии ресурсов.

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

HH> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...

HH>*Под абстракцией понимается выделение существенного.
Солнца клонилось к закату, а старушки все падали, и падали из окон... а математики, все искали и искали серебряннную пулю...

Здравствуйте, HrorH, Вы писали:

HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.

Золотые слова. Работа программиста сравнима с работой инженера проектирующего самолет, но при этом обладает таким вреднейшим качеством, как кажущаяся легкость модификации уже сделанного. Вторая проблема программирования: обычно человек видит сразу решения каких-то частных областей, зависящих от его собственного склада ума. Кто-то сразу видит общую архитектуру, придавая крайне малое значение деталям реализации; кто-то видит реализацию отдельных частей алгоритма, упуская общую архитектуру. Начиная работать с программой, человек начинает с именно с областей наиболее близких ему, генерируя заплатки в тех местах, которые кажутся ему не столь важными. Во что это все выливается — все вы прекрасно знаете.

Сравните это с работой инженера, который вынужден прорабатывать все изначально, перед тем как готовые чертежи уйдут на заводы. Цена ошибки тут велика и может вылиться в миллионы рублей/долларов. По сути инженер в чертежах, схемах, диаграммах как раз строит этакую полную модель будущего изделия, которой так не хватает программистам.

Ошибка работы программиста тоже очень велика и тоже очень часто выливается в огромные убытки. Но из-за некой "виртуальности" или "несерьезности" его работы, кажущейся ему самому и его начальству, мало кто удосуживается достаточным проектированием будущей программы. Движимые принципом "лучше быстрее, чем качественнее" мы роняем наши "самолеты", пускаем под откос "поезда", но все это сходит нам с рук. А ведь программирование — это в меньшей мере искусство, и в большей — наука. Тенденций к исправлению тоже не видно. Печально.

Здравствуйте, HrorH, Вы писали:


HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?
В самом устройстве человека?

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.

HH> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
HH> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
HH> 3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель, в противном случае количество вариантов будет слишком большим для такого анализа. Например, нужен анализ всех вариантов одновременных операций при доступе нескольких пользователей к иерархии ресурсов.
Бюджет и сроки любого проекта ограничены, поэтому перебрать все варианты зачастую просто невозможно. Поэтому берется модель которая устраивает всех(почти) и реализуется

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

HH> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...
Нет ни одной области человеческой деятельности где бы не было ошибок. Похоже это невозможно.

Над этой задачей работает много исследователей, и успехи тоже есть. Есть я зыки которые позволяют верифицировать определенные контракты.

К сожалению , очень часто на практике, трудностью является создание формального описания для решения задачи. Т.е. уже на этапе построения спецификации мы не можем избавиться от человеческих ошибок и плохой эфективности.

Зато в областях где каждая ошибка стоит очень дорого, применяются соответствующие интсрументы. Например верификация микросхем и т.п.

Здравствуйте, HrorH, Вы писали:

Спасибо за тему. Вопрос конечно стар как мир, что как бы намекает, но всё же.

Первое. Человеку свойственно ошибаться — смеритесь. Иногда какой-нибудь Фобос-Грунт будет падать и вывод здесь только один — то, что ошибка может случиться должно быть предусмотренно заранее. Где-то помнится проскальзывала история о том, как код на каком-то марсоходе дебажили удалённо, тобишь с Земли. Гениально! Так и надо.

Второе. Сложность задачи, которую может охватить человек, ограничена. Проше и дешевле (хотя, вследствии неграммотного руководства, невсегда) написать программу и посмотреть, что будет. Помните как Эдисон изобрёл лампочку — просто тупо пробовал все варианты. И знаете что — это сработало. Программировать — это не здание строить. Пробовать разные варианты здесь дёшево.

Третье. Мы всё ещё используем слишком низкоуровневые языки программирования. Чтобы вместить сложные задачи в голову человека, надо поднимать уровень абстракции. (Xотя сначало надо долго и нудно впихивать эти абстракции в голову самого человека. Начиная с "у меня было два яблока, одно отдал, сколько осталось?". А это я о чём? Правильно — об образовании). Иными словами надо улучшать инструменты, точнее использовать другие языки программирования. Будущее проблескивает где-то за декларативными языками программирования. Точнее к сожалению выразиться не могу. Так мне подсказывает моя программистская интуиция. Пока мои собственные попытки как-то собрать свои разрозненные мысли по субжекту терпят неудачу. Нахожусь в постоянной погоне за идеальной программой. Жду просветления.

Здравствуйте, HrorH, Вы писали:

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?
Прочитайте Дисциплину программирования Эдсгера Дейкстры.
А после нее — Наука программирования Дэвида Гриса.

И конечно примеры.
http://www.theengineer.co.uk/news/safer-software/312631.article

Здравствуйте, HrorH, Вы писали:

HH> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...

Дома строят уже сотни тысяч лет, а ошибки всё совершают и совершают.

Программы без ошибок появятся, когда появится искусственный интеллект.

Здравствуйте, vsb, Вы писали:

vsb>Здравствуйте, HrorH, Вы писали:

HH>> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...

vsb>Дома строят уже сотни тысяч лет, а ошибки всё совершают и совершают.

vsb>Программы без ошибок появятся, когда появится искусственный интеллект.

ИИ не "появится", его создадут. И тоже с ошибками...

Здравствуйте, Artifact, Вы писали:

A>Здравствуйте, HrorH, Вы писали:

A>Спасибо за тему. Вопрос конечно стар как мир, что как бы намекает, но всё же.

Вам спасибо, что это кому-то интересно.

A>Первое. Человеку свойственно ошибаться — смеритесь. Иногда какой-нибудь Фобос-Грунт будет падать и вывод здесь только один — то, что ошибка может случиться должно быть предусмотренно заранее. Где-то помнится проскальзывала история о том, как код на каком-то марсоходе дебажили удалённо, тобишь с Земли. Гениально! Так и надо.

Попробуете доказать, что человеку свойственно ошибаться?

Если серьезно, то каждая ошибка всегда имеет конкретную причину, я попытался выявить список таких причин в первом посте.

A>Второе. Сложность задачи, которую может охватить человек, ограничена. Проше и дешевле (хотя, вследствии неграммотного руководства, невсегда) написать программу и посмотреть, что будет. Помните как Эдисон изобрёл лампочку — просто тупо пробовал все варианты. И знаете что — это сработало. Программировать — это не здание строить. Пробовать разные варианты здесь дёшево.

То, что сложность задачи, которую может охватить человек, ограничена, почему-то не так мешает в других областях. Тут уже писали про инженера.
Пробовать разные варианты, это хорошо в случае, когда надо, чтобы работал хотя бы один вариант. Программа должна работать для всех возможных вариантов использования.

A>Третье. Мы всё ещё используем слишком низкоуровневые языки программирования. Чтобы вместить сложные задачи в голову человека, надо поднимать уровень абстракции. (Xотя сначало надо долго и нудно впихивать эти абстракции в голову самого человека. Начиная с "у меня было два яблока, одно отдал, сколько осталось?". А это я о чём? Правильно — об образовании). Иными словами надо улучшать инструменты, точнее использовать другие языки программирования. Будущее проблескивает где-то за декларативными языками программирования. Точнее к сожалению выразиться не могу. Так мне подсказывает моя программистская интуиция. Пока мои собственные попытки как-то собрать свои разрозненные мысли по субжекту терпят неудачу. Нахожусь в постоянной погоне за идеальной программой. Жду просветления.

Насчет декларативных языков, мне тоже так кажется.
Иногда хочется чего-то в духе Denotational design with type class morphisms

HH> Причем не только баги-описки, но баги в самой логике работы программы.
HH> Зачастую оказывается, что используемая модель некорректна даже в теории, при этом на практике она может даже более-менее успешно работать за счет каких-нибудь хакерских методов.
Вообще-то как раз описки — дело пустяковое. А вот отсутствие самой теории, скорей закономерность.

HH> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
Сформулируйте математически предметную область бухгалтерского учета, управления бизнес-процессами, работы с клиентами.
Чтобы доказать теоремы.

HH> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
Сложно учесть то, что появляется ПОСЛЕ ввода системы в эксплуатацию.
Но даже до ввода — покажите затраты применимости проектирования каждой операции в обычном таком опердене.

HH> 3) Не осуществляется полный анализ всех возможных вариантов.
Как бы да. Математики наплодили всяких разговоров о P и NP. Нет чтобы на парочке A4 проанализировать все варианты.

HH>Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель,
К ответу на п1:
А математики уже решили уравнения Навье-Стокса? Или задачу о трех(всего лишь!) телах?

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
У математиков точно нет. Математики вообще не занимаются проектированием.
Инженеры да, весьма часто прибегают к математике при проектировании. Но вот странно — почему-то есть хорошо спроектированные самолеты и мосты, а почему-то плохо. Может потому что в проектировании чего-либо немало от шаманства?
Чего уж говорить о выражении своих мыслей на формализованном языке программирования. Да, работающая программа обладает рядом свойств которые можно зафиксировать и количественно и качественно. Вот только тут как в китайской присказке — "На ковре с утками не найдешь иглы ее вышивавшей"

HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?
Может.
Осталась малость — заставить программистов=людей мыслить по этому паттерну.
А вот тут проблемы озвучены уже наверное с 3 лет.
1. почему человек рассудив что правильно — поступает неправильно.
2. И почему человек не хозяин собственным мыслям.

HH> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...
Программирование — в первую очередь прикладная область. А значит все в этой области:
1. отражение неразрешенных (а может и неразрешимых) проблем в чисто абстрактных дисциплинах — в первую очередь математике
2. влияние действительно мира, закономерности которого могут быть изучены неверно, или неизвестны.

HH>*Под абстракцией понимается выделение существенного.
... за счет отбрасывания несущественных деталей.
Покажите только безошибочную методику отделения существенного от несущественного и сразу счастья всем прибавится.

Здравствуйте, minorlogic, Вы писали:

Можно еще Степанова с "Элементами программирование почитать". А Gries да, хорош, не читал пока, но
содержание книжки внушает.

Здравствуйте, HrorH, Вы писали:

HH>То, что сложность задачи, которую может охватить человек, ограничена, почему-то не так мешает в других областях. Тут уже писали про инженера.

С чего Вы взяли, что не мешает? Те же инженеры, проектирующие самолеты, регулярно ошибаются. Причем эти ошибки бывают что доходят до производства и иногда приводят к гибели людей. А бывает, что становятся просто особенностями, слабостями самолета, с которыми обслуживающий персонал просто живет.

Здравствуйте, HrorH, Вы писали:

HH>Программа должна работать для всех возможных вариантов использования.
Позвольте не согласиться. Я считаю, что правильнее и надёжнее для каждого варианта писать отдельную программу.

Здравствуйте, HrorH, Вы писали:

A>>Первое. Человеку свойственно ошибаться — смеритесь. Иногда какой-нибудь Фобос-Грунт будет падать и вывод здесь только один — то, что ошибка может случиться должно быть предусмотренно заранее. Где-то помнится проскальзывала история о том, как код на каком-то марсоходе дебажили удалённо, тобишь с Земли. Гениально! Так и надо.

HH>Попробуете доказать, что человеку свойственно ошибаться?

Человеку свойственно переводить явления природы в систему символов (слова, цифры, команды языка программирования). Поскольку система символов — это лишь аппроксимация явлений окружающего мира, эта аппроксимация всегда выполняется с некоторыми неточностями. Отсюда вывод, что ошибки в рассуждениях, в моделировании, в процессе разработки — явление неизбежное, как следствие самой аппроксимации.

Когда программист пишет программу, он (как и любой другой специалист) проводит двойное преобразование: задание превращается в мыслительную модель, а эта модель уже воплощается в коде. И то и другое — суть преобразование из одних символов в другие, при этом на обоих этапах возможны ошибки.

HH>Если серьезно, то каждая ошибка всегда имеет конкретную причину, я попытался выявить список таких причин в первом посте.

Да, только эта причина устанавливается после проявления ошибки. Ошибки могут быть и в матмоделях, и в инвариантах, и во всём остальном. Притом больше того, у каждой ошибки есть не только причина, но ещё и имя с фамилией, и зачастую — не одно.

A>>Второе. Сложность задачи, которую может охватить человек, ограничена. Проше и дешевле (хотя, вследствии неграммотного руководства, невсегда) написать программу и посмотреть, что будет. Помните как Эдисон изобрёл лампочку — просто тупо пробовал все варианты. И знаете что — это сработало. Программировать — это не здание строить. Пробовать разные варианты здесь дёшево.

HH>То, что сложность задачи, которую может охватить человек, ограничена, почему-то не так мешает в других областях. Тут уже писали про инженера.

Мешает. Только в других областях перед "серийным производством" принято выписывать требования, тщательно верифицировать конструкторские решения и вообще всяко проверять друг друга. Это только в программировании принято уповать на "паттерны" чего бы то ни было — то на паттерны архитектур. то на паттерны мышления

HH>Пробовать разные варианты, это хорошо в случае, когда надо, чтобы работал хотя бы один вариант. Программа должна работать для всех возможных вариантов использования.

Программа и так всегда работает во всех вариантах использования. Просто в некоторых случаях её работа считается отклоняющейся от спецификации. А некоторые случаи считаются недопустимыми. Эту проблему, в принципе, могут помочь решить языки с автоматической проверкой корректности программы по отношению к формальной спецификации, Но ни один такой язык не защитит от ошибок в самой спецификации.

Здравствуйте, Skynin, Вы писали:

HH>> Причем не только баги-описки, но баги в самой логике работы программы.
HH>> Зачастую оказывается, что используемая модель некорректна даже в теории, при этом на практике она может даже более-менее успешно работать за счет каких-нибудь хакерских методов.
S>Вообще-то как раз описки — дело пустяковое. А вот отсутствие самой теории, скорей закономерность.

Согласен, причем закономерность печальная.

HH>> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
S>Сформулируйте математически предметную область бухгалтерского учета, управления бизнес-процессами, работы с клиентами.
S>Чтобы доказать теоремы.

При такой общей постановке технического задания не то что математическую модель, а даже самую кривую программу не написать.
Если же поставить конкретные задачи, то некоторые умные люди уже сейчас для многих из них смогут подобрать полезные модели.

HH>> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
S>Сложно учесть то, что появляется ПОСЛЕ ввода системы в эксплуатацию.
S>Но даже до ввода — покажите затраты применимости проектирования каждой операции в обычном таком опердене.

Наверно не покажу. Хотя бы потому, что не очень понимаю, что есть опердень. И что есть затраты применимости проектирования.

HH>> 3) Не осуществляется полный анализ всех возможных вариантов.
S>Как бы да. Математики наплодили всяких разговоров о P и NP. Нет чтобы на парочке A4 проанализировать все варианты.

Я так понимаю, что эти разговоры не мешают рассмативать задачи с конечным числом вариантов, которые очень часто встречаются на практике.
В этом топике приводили ссылку на доказательтство корректности ядра операционной системы или чего-то такого.

HH>>Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель,
S>К ответу на п1:
S>А математики уже решили уравнения Навье-Стокса? Или задачу о трех(всего лишь!) телах?

И что из этого следует? Что нельзя решить никакую задачу?

HH>> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
S>У математиков точно нет. Математики вообще не занимаются проектированием.
S>Инженеры да, весьма часто прибегают к математике при проектировании. Но вот странно — почему-то есть хорошо спроектированные самолеты и мосты, а почему-то плохо. Может потому что в проектировании чего-либо немало от шаманства?
S>Чего уж говорить о выражении своих мыслей на формализованном языке программирования. Да, работающая программа обладает рядом свойств которые можно зафиксировать и количественно и качественно. Вот только тут как в китайской присказке — "На ковре с утками не найдешь иглы ее вышивавшей"

HH>> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?
S>Может.
S>Осталась малость — заставить программистов=людей мыслить по этому паттерну.
S>А вот тут проблемы озвучены уже наверное с 3 лет.
S>1. почему человек рассудив что правильно — поступает неправильно.
S>2. И почему человек не хозяин собственным мыслям.

Философия — это хорошо, когда она на своем месте. "Доктор, я буду жить?" — "А смысл?"

HH>> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...
S>Программирование — в первую очередь прикладная область. А значит все в этой области:
S>1. отражение неразрешенных (а может и неразрешимых) проблем в чисто абстрактных дисциплинах — в первую очередь математике
S>2. влияние действительно мира, закономерности которого могут быть изучены неверно, или неизвестны.

Да, да. Программирование непознаваемо, закономерности действительного мира изучены неверно, все проблемы неразрешимы.
Может быть вернемся к практике, где вполне возможно просчитать и предусмотреть очень многие проблемы, и для этого не хватает только знаний и возможно, желания?

HH>>*Под абстракцией понимается выделение существенного.
S>... за счет отбрасывания несущественных деталей.
S>Покажите только безошибочную методику отделения существенного от несущественного и сразу счастья всем прибавится.

Не надо философии, в каждом случае требуется математическая модель, которая решает данные конкретные проблемы, а не все проблемы мира.

Здравствуйте, Геннадий Васильев, Вы писали:

ГВ>Здравствуйте, HrorH, Вы писали:

HH>>Попробуете доказать, что человеку свойственно ошибаться?

ГВ>Человеку свойственно переводить явления природы в систему символов (слова, цифры, команды языка программирования). Поскольку система символов — это лишь аппроксимация явлений окружающего мира, эта аппроксимация всегда выполняется с некоторыми неточностями. Отсюда вывод, что ошибки в рассуждениях, в моделировании, в процессе разработки — явление неизбежное, как следствие самой аппроксимации.

ГВ>Когда программист пишет программу, он (как и любой другой специалист) проводит двойное преобразование: задание превращается в мыслительную модель, а эта модель уже воплощается в коде. И то и другое — суть преобразование из одних символов в другие, при этом на обоих этапах возможны ошибки.

Хорошо, давайте говорить только о том классе ошибок, которые можно отловить, создав математическую модель и т.д. Ошибки, которые для своего разрешения требуют йогических практик, впадения в нирвану, и непосредственного созерцания Божественной Истины, рассматривать не будем.

HH>>Если серьезно, то каждая ошибка всегда имеет конкретную причину, я попытался выявить список таких причин в первом посте.

ГВ>Да, только эта причина устанавливается после проявления ошибки. Ошибки могут быть и в матмоделях, и в инвариантах, и во всём остальном. Притом больше того, у каждой ошибки есть не только причина, но ещё и имя с фамилией, и зачастую — не одно.

Устанавливается причина после проявления ошибки, но поняв ее, можно попытаться больше не совершать таких ошибок. И ошибка не в фамилии, а в неверном алгоритме мышления.

HH>>То, что сложность задачи, которую может охватить человек, ограничена, почему-то не так мешает в других областях. Тут уже писали про инженера.

ГВ>Мешает. Только в других областях перед "серийным производством" принято выписывать требования, тщательно верифицировать конструкторские решения и вообще всяко проверять друг друга. Это только в программировании принято уповать на "паттерны" чего бы то ни было — то на паттерны архитектур. то на паттерны мышления

Блин, никто не умеет читать. Я написал "не так мешает". Все почему-то прочли "не мешает". Кстати об ошибках
Понятно, что паттерны мышления не всемогущи, но они могли бы помочь совершать меньше ошибок.

HH>>Пробовать разные варианты, это хорошо в случае, когда надо, чтобы работал хотя бы один вариант. Программа должна работать для всех возможных вариантов использования.

ГВ>Программа и так всегда работает во всех вариантах использования. Просто в некоторых случаях её работа считается отклоняющейся от спецификации. А некоторые случаи считаются недопустимыми. Эту проблему, в принципе, могут помочь решить языки с автоматической проверкой корректности программы по отношению к формальной спецификации, Но ни один такой язык не защитит от ошибок в самой спецификации.

Да, зато от этих ошибок, по-крайней мере от многих из них можно попытаться защититься другими способами (о которых я попытался написать в первом посте).

Здравствуйте, Artifact, Вы писали:

HH>>Программа должна работать для всех возможных вариантов использования.
A>Позвольте не согласиться. Я считаю, что правильнее и надёжнее для каждого варианта писать отдельную программу.

А как же повторное использование кода?
Или это была шутка?

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

предсказания, полнота, однородность кода, разнообразие перепроверок

Ошибки появляются в следствии следующих причин:
1. "а это вообще должно было работать?"
2. неверная модель
3. забыты или нерассмотренны какие-то варианты поведения кода
4. опечатка

Ошибки первого рода возникают, когда программист даже не пытается обосновать и доказать правильность работы свое кода.
Ошибки второго рода провоцирует наше незнание, например, незнание — что требования к многопоточному коду отличаются от требований к однопоточному коду.
"Темные углы", они же вырожденные и частные случаи, и их нерасмотрение приводит к ошибкам третьего рода.
Опечатки заложены в природе человека, и даже так и называются — "человеческий фактор". Опечатки уменьшаются при концентрации всего внимания на одной задаче, но полностью от них избавиться не получается.

Для борьбы с этими ошибками есть стандартные рекомендации: пишите правильный код, много знайте, ничего не забывайте, и не теряйте концентрацию когда пишите код. Проблема этих рекомендаций: что они не говорят — а как это сделать?, и не говорят — а как убедиться: что правильности кода уже достаточно? что знаний о ситуации уже достаточно? что достаточно всего вспомнено? и что концентрации внимания тоже достаточно?

Стандартные рекомендации стоит подкрепить следующими привычками:

Предсказание. Основная привычка для защиты от ошибок: это привычка предсказывать поведение своего и чужого кода до запуска кода.
Всегда сначала пытаемся предсказать, как должен себя вести данный код: за сколько времени отработает, что выведет на экран, в каком порядке будут вызываться строки кода, какие будут промежуточные данные и т.д. (чем больше всяких предсказаний, тем лучше).
Потом код запускаем и проверяем свои предсказания, и если предсказанное не совпало с ожидаемым, то разбираемся почему наше представление не совпало с реальностью.

Полнота. Вторая привычка: предсказывать и рассматривать поведение на всем множестве внешних факторов, включая самые худшие сценарии (например, если читается файл определенный структуры, то каким будет поведение кода, если какие-то байты будут случайно изменены, или вообще, если файл сформирован "злоумышленником", который хочет наш код "завалить"?)
Здесь главное не надо бросаться в избыточность: явно фиксировать и обрабатывать в коде все возможные ошибки. достаточно, чтобы код вел себя адекватно: не портит данные, на ошибочную ситуацию формирует ошибку, не скрывает информацию по ошибке.

Разнообразие перепроверок. В большинстве случаев, нет гарантированного способа определить: достаточное или недостаточное кол-во предсказаний уже сделано, чтобы обеспечить правильность нашего представления?. Достаточно (или недостаточно) рассмотрено вариантов? Достаточно или недостаточно написано тестов? есть в коде опечатки или нет? и т.д. Здесь можно лишь рассчитывать на корреляцию, что чем больше разнообразных вариантов перепроверено, и не выявлено проблем, то тем больше вероятность, что наше представление и код правильный. Большинство действий по перепроверке рутинные и их можно переложить на компьютер: статическая типизация, регрессионное тестирование, проверка покрытие кода тестами, проверка, что у кода "хороший запах" и т.д.

Однородность кода. Если придерживаться предыдущих трех правил, то кол-во рассматриваемых вариантов растет лавинообразно по экспонециальному закону. Лавину можно минимизировать, если стараться писать однородный код.
возьмем два кода

for (uint i = items.Length - 1; i >= 0; --i)
{
  var item = items[i];
  //что-то делаем с item
}

и

foreach (var item in items.Reverse())
{
  //что-то делаем с item
}

второй код более однородный, чем первый. в первом коде, для полноты необходимо рассматривать поведение i на границах: что надо написать, чтобы перебрать концевые элементы и при этом не выйти за границу массива: items.Length или items.Length — 1, и i >= 0 или i > 0; также необходимо проверить как себя ведет i "по ту сторону границы", и только вот здесь обнаружится ошибка..
второй код этого всего не имеет, потому что оно уже "спрятано" внутрь функции Reverse, и все эти варианты были рассмотрены при написании функции Reverse.

Привычки предсказывать и перепроверять предсказания уменьшает вероятность появление ошибок первого и второго рода. Привычка к однородному коду с перепроверкой уменьшает кол-во невыявленных опечаток. Привычка к полноте с перепроверкой уменьшает ошибки второго и третьего рода.

Здравствуйте, Васильич, Вы писали:

В>Золотые слова. Работа программиста сравнима с работой инженера проектирующего самолет, но при этом обладает таким вреднейшим качеством, как кажущаяся легкость модификации уже сделанного.

Совершенно согласен, хотя никак не могу понять, почему же математики не производят аналогичного говнища, несмотря на то, что "легкость модификации" результатов их труда вполне сопоставима.

I> почему же математики не производят аналогичного говнища, несмотря на то, что "легкость модификации" результатов их труда вполне сопоставима.

это вызвано лишь ошибкой твоего восприятия: с ошибками программ ты встречаешься каждый день, а с ошибками математиков ты не встречаешься.
взять хотя бы теорему ферма — за последние сто лет разного рода математиками было сформированы, наверное, миллионы доказательств ее правильности и все они оказались неверными, кроме последнего.

Здравствуйте, HrorH, Вы писали:

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

Если рассматривать программирование через призму управления сложностью, то всё получается гораздо лучше, чем обычно.

Здравствуйте, IT, Вы писали:

IT>Здравствуйте, HrorH, Вы писали:

HH>> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH>> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

IT>Если рассматривать программирование через призму управления сложностью, то всё получается гораздо лучше, чем обычно.

Извините, можно для тупых поподробнее или может быть ссылки на какую-то литературу.

Здравствуйте, VsevolodC, Вы писали:

VC>Здравствуйте, vsb, Вы писали:

vsb>>Программы без ошибок появятся, когда появится искусственный интеллект.

VC>ИИ не "появится", его создадут. И тоже с ошибками...

При этом способность совершать ошибки будет заложена в сам ИИ

Здравствуйте, DarkGray, Вы писали:

DG>это вызвано лишь ошибкой твоего восприятия: с ошибками программ ты встречаешься каждый день, а с ошибками математиков ты не встречаешься.

По-моему это самоуспокоение, тем более, что таким же образом можно попытаться убедить меня, что и у инженеров ошибок не меньше, но ведь это уж точно не так, о том, как работают инженеры какое-никакое представление у меня есть.

Здравствуйте, HrorH, Вы писали:

IT>>Если рассматривать программирование через призму управления сложностью, то всё получается гораздо лучше, чем обычно.
HH>Извините, можно для тупых поподробнее или может быть ссылки на какую-то литературу.

Закон сохранения сложности

Автор(ы): Игорь Ткачёв
Дата: 06.12.2002

.

Здравствуйте, HrorH, Вы писали:

HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.

А если это не так и причина в другом? Делая какое-то конечное умозаключение останавливаем мыслительный процесс, чтобы сказать что-то на вроде

HH> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...

возможно через сто лет. Почему сто лет, почему не сейчас? Зачем ждать сто лет, тем более, что большинство явно не доживёт?

I>о том, как работают инженеры какое-никакое представление у меня есть.

ты свой единичный опыт, что инженеры работают "лучше", чем программисты — распространяешь на всю отрасль: что все инженеры работают лучше, чем программисты. на основании чего ты делаешь такой переход?

Шаттл с 6 космонавтами, например, взорвался по инженерным причинам, а не по программным.

При этом тот же Фейнман говорит, что это была не случайность, и что состояние инженерного комплекса было много хуже, чем программного.

В итоге хотелось бы заметить, что система проверки программного обеспечения компьютеров действительно показывает себя как высококачественная. Судя по всему, там нет места постепенному самообману путем снижения норм, что весьма характерно для систем безопасности твердотопливных ракета-носителей и основных двигателей шаттла. Для вящей убедительности добавлю, что руководство недавно предлагало прекратить такие сложные и дорогие испытания за их ненадобностью в последнее время истории запусков шаттла.

При этом с двигателями было все намного хуже:

За 250 000 секунд работы основные двигатели отказывали, вероятно, раз 16.

Список некоторых проблем (и их состояния):
Трещины лопаток турбины в топливных турбонасосах высокого давления (ТТНВД). (Возможно, решена.)
Трещины лопаток турбины в кислородных турбонасосах высокого давления (КТНВД). (Не решена.)
Пробой линии форсажного искрового воспламенителя (ФИВ). (Возможно, решена.)
Отказ контрольного вентиля для выпуска газов. (Вероятно, решена.)
Эрозия корпуса ФИВ. (Вероятно, решена.)
Растрескивание листового металла корпуса турбины ТТНВД. (Вероятно, решена.)
Повреждение футеровки труб для охлаждения ТТНВД. (Вероятно, решена.)
Отказ выходного коленчатого патрубка основной камеры сгорания. (Вероятно, решена.)
Смещение сварного шва входного коленчатого патрубка основной камеры сгорания. (Вероятно, решена.)
Субсинхронный вихрь КТНВД. (Вероятно, решена.)
Система аварийного отключения ускорения полета (частичный отказ системы с резервированием). (Вероятно, решена.)
Растрескивание подшипников. (Частично решена.)
Вибрация с частотой 4 000 герц, которая приводит некоторые двигатели в нерабочее состояние. (Не решена.)



Многие из этих, на первый взгляд, решенных проблем были видны уже на ранних стадиях использования новой конструкции: 13 из них появились в первые 125 000 секунд эксплуатации двигателя и только 3 – во вторые 125 000 секунд. Естественно, никогда нельзя быть уверенным, что все недостатки устранены; однако, возможно, в отношении некоторых недостатков стремились устранить не ту причину. Вполне разумно предположить, что в следующие 250000 секунд может произойти, по крайней мере, один сюрприз: вероятность равна 1/500 на двигатель на задание.

[..]

Инженеры в Рокетдайне, где производятся двигатели, оценивают полную вероятность как 1/10 000. Инженеры в Маршалле оценивают ее как 1/300, тогда как руководство НАСА, которому эти инженеры отправляют свои отчеты, утверждает, что вероятность равна 1/100 000. Независимый инженер, дающий НАСА консультации, счел разумной оценкой 1 или 2 к 100

[..]

Медленный сдвиг в направлении снижения коэффициента безопасности можно увидеть во множестве примеров.

http://scilib.narod.ru/Physics/Feynman/WDYC/ru/feyinman.html#TOC_id2994316

Основная разница: это есть ли ОТК и как он построен. У инженеров есть лишь преимущество, что они на 100 лет больше потратили на выстраивание ОТК для проверки качества своей работы. А также сложностью входа на инженерный рынок: большинство решений делается уже существующими компаниями, у которых наработана школа ОТК. в программировании из-за его сильной изменчивости и низкого порога входа: есть большая доля новичков, которые не имеют выстроенного подхода к ОТК. В тоже время большое кол-во новичков и низкий порог входа обеспечивает бурное развитие отрасли.

добавлю, что очень важный показатель надежности системы: это запас прочности.
при этом в инженерной отрасли не ставится под сомнение необходимость такого запаса.

в программировании же до сих пор многие считают, что запас прочности это неважно — и используют тот же C/C++, которые не имеет запаса прочности вообще, и любая малейшая ошибка может привести к произвольным катастрофическим последствиям.

Здравствуйте, DarkGray, Вы писали:

DG>ты свой единичный опыт, что инженеры работают "лучше", чем программисты — распространяешь на всю отрасль: что все инженеры работают лучше, чем программисты. на основании чего ты делаешь такой переход?

По меньшей мере половина проблем возникавших со всякими электронными штуковинами, которыми я пользовался, были софтверного, а не хардверного характера. Причем повседневную битву с (Windows) компьютером, на работе или дома я не считаю, не считаю также и проблемы неудобства пользования, в конце концов это субъективно. Только зависания, неожиданные перезагрузки и т.п. Вот возьмем мобильный телефон, там и компьютер, и радиопередатчик, и дисплей, и аккумулятор, все на таком уровне, который еще 20 лет назад был недостижим. Это же хайтек не хуже космоса и ядреного оружия, просто продается за копейки по причине массового производства. И все ведь работает как часы, проблемы только с говняным софтом. А что в софте том такого сложного?

Здравствуйте, DarkGray, Вы писали:

DG>которые не имеет запаса прочности вообще, и любая малейшая ошибка может привести к произвольным катастрофическим последствиям.

а Вы не могли бы по подробнее?..

Здравствуйте, DarkGray, Вы писали:

DG>в программировании же до сих пор многие считают, что запас прочности это неважно — и используют тот же C/C++, которые не имеет запаса прочности вообще, и любая малейшая ошибка может привести к произвольным катастрофическим последствиям.

C++ говоришь? А вот у меня был телефон Siemens, так тот иногда начинал вдруг крайне медленно реагировать, похоже мусор собирал, гад.

Здравствуйте, HrorH, Вы писали:

HH>А как же повторное использование кода?
С повторным использованием всё впорядке. Предполагается, что программа состоит из большого числа узлов, блоков, назовите как угодно. Каждый узел получает, что-то на вход и отдаёт что-то на выходе. По факту это принцип электросхемы. Аналогично Юникс пайпс, язык FP Джона Бэкуса, APL.

HH>Или это была шутка?
Нет, но смеяться можно

I> А что в софте том такого сложного?

кол-во вариантов, которые необходимо разобрать и предусмотреть.

I>Только зависания, неожиданные перезагрузки и т.п.

непонятно, почему ты считаешь, что это чисто софтварные проблемы.
это может быть вызвано вплоть до физических проблем, когда состояние бита меняется космическим излучением.
насколько я помню, для не ECC-памяти — это оценивается как три случая в год при непрерывной работе устройства.

Здравствуйте, HrorH, Вы писали:
HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок? В чем причина ошибок?

Если предположить, что багов не должно быть вообще, то создание программы вырождается в нерешаемую задачу. Баги не побочный эффект программирования, баги это необходимый элемент программы. Собственно, любую программу можно представить как набор [потенциальных] багов.

Собственно, не стоит воспринимать баги как ошибки. Думаю, стоит говорить о недоработках.

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.

А вот это тебе только кажется. Если бы писали то, что приходит в голову, жизнь была бы чудесной. Я не знаю, куда приходит то, что обычно пишут в коде, но это явно не голова.

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

Нет. Нет.

Здравствуйте, IT, Вы писали:
IT>Если рассматривать программирование через призму управления сложностью, то всё получается гораздо лучше, чем обычно.

Если рассматривать программирование через призму управления сложностью, то либо ошибок нет вообще в принципе, либо любая конструкция по дефолту является ошибкой.

Здравствуйте, DarkGray, Вы писали:

DG>непонятно, почему ты считаешь, что это чисто софтварные проблемы.
DG>это может быть вызвано вплоть до физических проблем, когда состояние бита меняется космическим излучением.
DG>насколько я помню, для не ECC-памяти — это оценивается как три случая в год при непрерывной работе устройства.

Не, ну я ж профи. Проблемы-то повторяются, во многих случаях я их репродуцировать могу.

Здравствуйте, Ромашка, Вы писали:

IT>>Если рассматривать программирование через призму управления сложностью, то всё получается гораздо лучше, чем обычно.
Р>Если рассматривать программирование через призму управления сложностью, то либо ошибок нет вообще в принципе, либо любая конструкция по дефолту является ошибкой.

Не вижу в твоём утверждении логической связи между тем, что после 'если' и после 'то'.

DG>>которые не имеет запаса прочности вообще, и любая малейшая ошибка может привести к произвольным катастрофическим последствиям.

S>а Вы не могли бы по подробнее?..

запас прочности можно рассматривать как минимизацию функции F, где F — это функция ухудшение работоспособности системы от сбоя (или изменения условий эксплуатации) отдельной части системы.
соответственно, для машины ожидается, что неисправность лампочки или прокол колеса не приводят к разносу двигателя.
для программы на C/C++ такого ожидания гарантировать нельзя, малейшая ошибка в самом некритическом коде может привести к "проезду по памяти" и отказу любого другого узла (сколько угодно критического), находящегося в той же самой памяти.
частично это проблема решается разнесением по отдельным процессам, что часто делается в nix-программах, но это имеет естественный предел: узлы можно разнести по 2-10 процессам(максимум тысячу), но миллион узлов уже друг от друга таким подходом не разнесешь.

Здравствуйте, HrorH, Вы писали:


Тише... Тише... Никому не рассказывай, что можно вообще не делать ошибок. Потому что для того чтобы не делать ошибок нужно реально решать NP-полные задачи. А человек этого сделать не может по определению. А значит это будут машины. А если они решают NP полные задачи, значит они же могут их и ставить, что в свою очередь NP полная задача. И любой холодильник или стиральная машина будет плевать в тебя машинным маслом: "Тупая органика". И любой пылесос тебе скажет: "убери за мной, тряпка недоразвитая". И сгинет человечество, как промежуточный этап эволюции, уже ненужный никому, и отслуживший своё. Так что, программист помни. Делая ошибки ты стоишь на страже человечества.

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?

Есть такое, гуглите по словам "defensive development".

Здравствуйте, HrorH, Вы писали:

HH>Хорошо, давайте говорить только о том классе ошибок, которые можно отловить, создав математическую модель и т.д. Ошибки, которые для своего разрешения требуют йогических практик, впадения в нирвану, и непосредственного созерцания Божественной Истины, рассматривать не будем.

Тогда мы автоматически исключаем те ошибки, которые будут связаны с неправильно выбранной математической моделью. То есть мы сузим круг поисков до: "Где светлей".

HH>>>Если серьезно, то каждая ошибка всегда имеет конкретную причину, я попытался выявить список таких причин в первом посте.
ГВ>>Да, только эта причина устанавливается после проявления ошибки. Ошибки могут быть и в матмоделях, и в инвариантах, и во всём остальном. Притом больше того, у каждой ошибки есть не только причина, но ещё и имя с фамилией, и зачастую — не одно.

HH>Устанавливается причина после проявления ошибки, но поняв ее, можно попытаться больше не совершать таких ошибок. И ошибка не в фамилии, а в неверном алгоритме мышления.

Я не вижу в первом предложении ни одного основания для утверждения: "ошибка... в неверном алгоритме мышления". Такие нарушения в логике изложения часто становятся причиной и ошибок, и ненужных затягиваний разработки.

HH>>>То, что сложность задачи, которую может охватить человек, ограничена, почему-то не так мешает в других областях. Тут уже писали про инженера.
ГВ>>Мешает. Только в других областях перед "серийным производством" принято выписывать требования, тщательно верифицировать конструкторские решения и вообще всяко проверять друг друга. Это только в программировании принято уповать на "паттерны" чего бы то ни было — то на паттерны архитектур. то на паттерны мышления

HH>Блин, никто не умеет читать. Я написал "не так мешает". Все почему-то прочли "не мешает". Кстати об ошибках

Плохой писатель обвиняет читателей в неумении читать, а хороший переформулирует мысль. Читать все умеют, просто ты употребил сравнение так, словно хочешь сказать, что в "других" областях пренебрежимо малы помехи, связанные с ограниченным объёмом человеческой головы. Да, это как раз об особенностях восприятия письменного текста: неудачно выбранная лексика создаёт массу сложностей в передаче информации от человека к человеку.

HH>Понятно, что паттерны мышления не всемогущи, но они могли бы помочь совершать меньше ошибок.

Может быть, только здесь придётся касаться очень глубоких индивидуальных вещей. Простейший источник ошибок: подумал, что всё ясно, а оказалось, что понял неправильно. Как предотвратить эту ситуацию? Можно пуститься в метафизику с выяснением градаций сомнений и спектра ощущений, которые сопутствуют той или иной степени уверенности. А можно пойти традиционным и надёжным путём: предписать детализировать всё, чтобы изложенное на бумаге не содержало противоречий и недосказанностей, а документы прогонять по одному-двум дополнительным review. Создать несколько томов типовых требований и способов их воплощений, чтоб не повторяться всякий раз, полученный продукт тщательно оттестировать, подписать акты приёмки... И никаких паттернов в голову заколачивать не надо, всё придумано и обкатано не один десяток лет назад.

HH>>>Пробовать разные варианты, это хорошо в случае, когда надо, чтобы работал хотя бы один вариант. Программа должна работать для всех возможных вариантов использования.

ГВ>>Программа и так всегда работает во всех вариантах использования. Просто в некоторых случаях её работа считается отклоняющейся от спецификации. А некоторые случаи считаются недопустимыми. Эту проблему, в принципе, могут помочь решить языки с автоматической проверкой корректности программы по отношению к формальной спецификации, Но ни один такой язык не защитит от ошибок в самой спецификации.

HH>Да, зато от этих ошибок, по-крайней мере от многих из них можно попытаться защититься другими способами (о которых я попытался написать в первом посте).

Я что-то не увидел в твоём первом посте описания способов защиты от ошибок — это раз. А два — надёжная защита надёжна потому, что работает вне зависимости от субъекта. Этим хороши разнообразные нормированные процедуры с разделением ответственностей: один пишет, другой вычитывает, третий принимает решение о "заходе на второй круг". Несколько специалистов пропустят ошибку с меньшей вероятностью, чем один. При условии, конечно, что они добросовестно выполняют свои обязанности, наделены соответствующими полномочиями и дееспособны в рамках этих полномочий.

Здравствуйте, HrorH, Вы писали:

HH> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.

Возможно, что формулировка мат. модели или детальный анализ предметной области окажется сложнее, чем написание программы.
В примитивных случаях: полным перебором можно найти решение, которое после строго обосновать и вывести формулу.
В более сложном: сделать несколько прототипов системы на простом языке.

Здравствуйте, HrorH, Вы писали:

HH>При такой общей постановке технического задания не то что математическую модель, а даже самую кривую программу не написать.
HH>Если же поставить конкретные задачи, то некоторые умные люди уже сейчас для многих из них смогут подобрать полезные модели.
Не могут, потому что таких моделей нет. Как там, в "Фактах и заблуждениях ..."
Бухгалтерские программы пишутся с 70ых годов, но поверьте, что в этот момент, когда вы читаете эти сроки пишутся новые, и с 10ок их уже близки к провалу.

Конкретные задачи имеют хорошие модели разве что вывод в консоль "Hello world"
Остальное — опыт, чутье, по аналогии с успешными.

HH>Наверно не покажу. Хотя бы потому, что не очень понимаю, что есть опердень. И что есть затраты применимости проектирования.
Опердень — банковское ПО "операционный день".

Но вы и складскую программу не спроектируете математике. Вернее — может быть и можно, но выйдет так дорого, причем не избавит от проблем при ее эксплуатации что нет смысла.

Понимаете, те "математики" что мне встречались сплошь говорят о тестировании алгоритмов. Причем простеньких, типа сортировки.
А работающая компьютерная программа есть конечный автомат с весьма приличным числом состояний. Причем на эти состояния влияют нередко — внешний условия.

HH>Я так понимаю, что эти разговоры не мешают рассмативать задачи с конечным числом вариантов, которые очень часто встречаются на практике.
На практике то как раз встречаются редко.
Хотя, пару миллиардов — да, тоже конечное число вариантов.

HH>В этом топике приводили ссылку на доказательтство корректности ядра операционной системы или чего-то такого.
Пропустил. Но пусть вначале драйвера научаться на корректность тестировать.

HH> И что из этого следует? Что нельзя решить никакую задачу?
Из этого следует что математика совсем не панацея если даже свои собственные проблемы не только не решила, а даже пока не придумала с какого боку за них браться.
А "через миллион лет", и "нельзя решить" для меня смертного тождественные выражения.

HH>Философия — это хорошо, когда она на своем месте. "Доктор, я буду жить?" — "А смысл?"
Ну так вы же развели бытовую философию

Я бы тоже лучше о практике послушал.

HH>Да, да. Программирование непознаваемо, закономерности действительного мира изучены неверно, все проблемы неразрешимы.
Я такого не утверждал.

HH>Может быть вернемся к практике, где вполне возможно просчитать и предусмотреть очень многие проблемы, и для этого не хватает только знаний и возможно, желания?
Так я пока ее от вас и не вижу. И за года в программировании много слышал о "математике" как средстве решения проблем, да только на практике как-то мало видел.

Так что повторюсь, вы не пожелания и мечты свои — а практику озвучьте.

HH>Не надо философии, в каждом случае требуется математическая модель, которая решает данные конкретные проблемы, а не все проблемы мира.
Не надо пустых слов, приведите примеры математических моделей для работающих компьютерных программ. Модели, по которым создавались эти программы.
Я вот почитал остальное обсуждение на момент написания этой строчки.
Где там конкретика?

А насчет философии, так вот мое ИМХО что большинство юных мечтателей о математике как решении проблем — как раз ею неумело пытаются подменить конкретную мозговую работу, как математиков так и инженеров.

Здравствуйте, Nuzhny, Вы писали:

N>Возможно, что формулировка мат. модели или детальный анализ предметной области окажется сложнее, чем написание программы.
Не возможно, а так и будет, поэтому то математиков ушли из отрасли еще в 70ых. Утрировано конечно. Встречается ПО где такой анализ обязателен и доныне — например сервера БД и их алгоритмы обработки данных.

N>В примитивных случаях: полным перебором можно найти решение, которое после строго обосновать и вывести формулу.
Решение — чего? Немногое число программ работает с данными полученными только на старте алгоритма.
А большинство программ в процессе работы запрашивают данные.
И собственно — а текст компьютерной программы разве не та самая конечная формула?

Перебор же собственно и используется при тестировании. Или вообще разработка ведется по TDD.
Так же собственно и математики поступают, когда не могут разрешить общий случай — прибегают к решению частных случаев.

N>В более сложном: сделать несколько прототипов системы на простом языке.
Делаются, как же без них. Только математика тут ни при чем — создание макета давно известно человечеству.

HH> Есть ли какой-то способ проектирования, который бы позволил если не избавиться от ошибок, то хотя бы минимизировать их число?
HH> Может ли существовать какой-то паттерн мышления, которому надо следовать, чтобы добиться этого?

В качестве средства описания мне до сих пор нравятся старые добрые структурно-информационные временные схемы (СИВС)...

Здравствуйте, os24ever, Вы писали:

O>В качестве средства описания мне до сих пор нравятся старые добрые структурно-информационные временные схемы (СИВС)...
И замечу что математики в них нет. Поэтому в таком, или ином виде и рисуются такие схемы. Это можно сказать обязательная часть проектирования.

Правда, до надежно работающей компьютерной программы от них еще весьма далеко.
Например из таких схем плохо видно — а области единых транзакций какие будут?

Мне вот другие картинки вспомнились из недавно встреченных.
Из статьи:
Engineering Management: Why are software development task estimations regularly off by a factor of 2-3?
Знание английского требуется минимальное, там все наглядно.

Так вот и реальный проект компьютерной программы что та береговая линия. И математика тут слабо поможет, потому что — ну вот такая она эта предметная область, кривая, косая, с массой исключений и уникальностей. И какой математикой будем проверять соответствие выбранных моделей — действительности?

Здравствуйте, Skynin, Вы писали:

S>Здравствуйте, os24ever, Вы писали:

O>>В качестве средства описания мне до сих пор нравятся старые добрые структурно-информационные временные схемы (СИВС)...
S>И замечу что математики в них нет. Поэтому в таком, или ином виде и рисуются такие схемы. Это можно сказать обязательная часть проектирования.

Не любите Вы математику

Если серьезно, то математическая модель у меня появляется (к сожалению) уже ближе к концу разработки программы, когда я уже четко представляю то, о чем пишу. В одном случае я использовал нотацию теории множеств, добавив в нее немного своей нотации. Получилось не вполне математически строго, но как не странно, эти формулы помогли мне найти ошибку в программе. Причем я отчетливо понимаю, что данная конкретная нотация может быть полезна только для данного случая (и аналогичных).
Если Вам не нравится математика, то модель не обязана быть строго математической, достаточно того, чтобы она помогала находить ошибки.
Настоящие же профи могут использовать настоящую математику (алгебру — моноиды, монады, аппликативные функторы и т.п.), причем достаточно сложную.
Я смотрю в сторону таких вещей как денотационная семантика, функциональное программирование.
Для примера можно привести библиотеку функционального реактивного программирования.

здесь блог автора реализации
здесь одна из статей по теории

Конечно, это уже высший пилотаж, и от всех людей нельзя требовать, чтобы они даже понимали о чем речь в этой статье.
Но библиотеку сделали именно по математической модели. Так что вполне возможно делать нетривиальные программы, используя математику.
Нам же, кто математику знает плохо, может быть полезна даже не очень строгая формулировка модели, лишь бы она помогала достичь полноты, о которой говорили выше.

Посмотрите также ссылку, которую давали выше, по теории сложности и SRP. Это интересно.

Здравствуйте, DarkGray, Вы писали:

DG>второй код более однородный, чем первый.

Неудачный пример. foreach проще for'а не потому что однороднее, а потому что использует меньше сущностей. Однородность это скорее стандартность, т.е. если похожие задачи мы по всему коду будем решать схожим образом, и в плане оформления и в плане построения алгоритма, то вероятность допустить ошибку снизится.

А принцип минимума сущностей должен идти в твоем списке отдельным пунктом, причем пожалуй самым важным. Т.к. тот же геттерный подход по сравнению с сеттерным снижает количество ошибок на порядок, чего никакими улучшениями "предсказаний, полноты, однородности кода, разнообразия перепроверок" добиться невозможно (при сопоставимых усилиях).

Здравствуйте, HrorH, Вы писали:

HH>Не любите Вы математику
Так это Ваше имя?

Я не люблю "математиков", а не математику.
Примерно как Linux уважаю, в вот "форумных линуксоидов" обычно — нет

HH>Если серьезно, то математическая модель у меня появляется (к сожалению) уже ближе к концу разработки программы, когда я уже четко представляю то, о чем пишу. ... Причем я отчетливо понимаю, что данная конкретная нотация может быть полезна только для данного случая (и аналогичных).
Если серьезно, то стоит назвать область в которой пишите программы. Как я вскользь упоминал — вполне представляю такие области, где применение строго математических методов будет эффективным.

HH>Если Вам не нравится математика, то модель не обязана быть строго математической, достаточно того, чтобы она помогала находить ошибки.
Повторюсь — мне не нравятся верующие. Математика не в состоянии помогать ошибки в программировании в подавляющем числе случаев.
В предыдущих постах бегло написал почему.

НЕ отождествяйте себя с математикой, я возражаю не ей, а Вашему ее идеализации

HH>Настоящие же профи могут использовать настоящую математику (алгебру — моноиды, монады, аппликативные функторы и т.п.), причем достаточно сложную.
А что такое настоящие профи, и ненастоящие?

ИМХО — настоящие профи весьма прагматичные ребята. И они используют инструменты что подходят под ситуацию, а не молятся на идеальные методики.

HH>Я смотрю в сторону таких вещей как денотационная семантика, функциональное программирование.
И какое это отношение имеет к природе ошибок в программировании?

HH>Для примера можно привести библиотеку функционального реактивного программирования.
Можно.
А смысл, если Вы не смогли показать "на пальцах" как разрешить основные причины ошибок в программировании своим подходом.

Для примера же могу привести тьму библиотек БЕЗ особой математики, но которые используются в тьме ПО. Замечу — работающего ПО, а не идеального, но которое идеально потому что оно вообще не вышло за стены "лаборатории", а возможно из головы автора.

HH>здесь блог автора реализации
HH>здесь одна из статей по теории

HH>Конечно, это уже высший пилотаж, и от всех людей нельзя требовать, чтобы они даже понимали о чем речь в этой статье.
Понимаете, ролики на ютьюбе с забрасывающими мяч в баскетбольную корзину с удивительных позиций набрали немалое число просмотров.
Только возьмут ли тех ребят в NBA?

"Высший пилотаж" понятие относительное.

HH>Но библиотеку сделали именно по математической модели. Так что вполне возможно делать нетривиальные программы, используя математику.
Я и не утверждал что нельзя.

И утрировано — меня интересуют больше: как писать тривиальное ПО без ошибок

HH>Нам же, кто математику знает плохо, может быть полезна даже не очень строгая формулировка модели,
Нам же, программистам, и строгая без толку.

HH>Посмотрите также ссылку, которую давали выше, по теории сложности и SRP. Это интересно.
На свете много чего интересного. И в программировании тоже.

Но я так и не увидел как математические модели могут помочь отрасли разработки ПО.

Добавлю, что увлечение ими было распространено в 50ые, 60ые, а в 80ые японцы даже провалили создание машин 5го поколения.

Программирование с тех пор стало циничней и скептичней.
Конечно, наработки в сomputer science продолжаются и востребованы. (а то еще может вы себя и с сomputer science отождествляете и скажете что я против)
Но до ошеломляющего успеха науки в практике — ой как далеко.

Более эффективными методами оказываются существующие и их развитие — грамотное управление ведением проектов, харизматичные менеджеры собирающие сплоченные команды, ООП, TDD и просто талант+квалификация программистов.

Математика — одна из самых формализованных дисциплин. И если ее формализация не работает, не помогает кардинально решить проблемы, то вот и возникает вопрос о ее применимости к таким-то проблемам вообще.

U>А принцип минимума сущностей должен идти в твоем списке отдельным пунктом, причем пожалуй самым важным. Т.к. тот же геттерный подход по сравнению с сеттерным

pull-схема(она же геттеры) улучшает предсказуемость кода. фактически при pull-схеме, что написано в коде, то и будет происходить в реальности, при push-схеме — реальное поведение необходимо восстанавливать.

зы
не вижу пока, как ты именно через переход сеттеры -> геттеры уменьшаешь кол-во сущностей.

Здравствуйте, HrorH, Вы писали:

HH> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
HH> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
HH> 3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель, в противном случае количество вариантов будет слишком большим для такого анализа. Например, нужен анализ всех вариантов одновременных операций при доступе нескольких пользователей к иерархии ресурсов.

Я бы сказал не хватает пункта 4 — нужно учитывать, что завтра могут поменяться требования и половину продукта придется перелопатить. Это очень печальный пункт, когда люди умудряются размазать логику по всем модулям, так что ее потом замучаешься вытаскивать

Здравствуйте, Skynin, Вы писали:

То, что Вы пишите, говорит о том, что Вы не понимаете меня. А я в свою очередь не могу понять Вас.
Я не знаю, как объяснить, потому что сам еще мало что понимаю.
Я пишу программы в области документооборота. Вам стало легче?
Те задачи, которые при этом возникают, не имеют к этому названию никакого отношения.
Математика — это всего лишь язык, инструмент, которым можно пользоваться.
Я порекомендовал модели, как одно из средств, которое позволяет избежать ошибок уже на этапе продумывания спецификации программы.
Использовать ли их, и в каких случаев, это дело каждого.
Я не собираюсь их навязывать.
Более того, я хотел бы узнать, какие вообще есть средства, чтобы минимизировать количество ошибок.

Здравствуйте, ZOI4, Вы писали:

ZOI>Здравствуйте, HrorH, Вы писали:

HH>> 1) Не формулируется математическая модель предметной области, не доказываются необходимые теоремы. Возможно не везде это требуется, но в нетривиальных случаях без этого не обойтись.
HH>> 2) Не учитываются свойства системы, о которых надо помнить при проектировании каждой операции (например, это могут быть такие свойства, как безопасность, одновременный доступ к ресурсам, блокировки, какие-то инварианты предметной области)
HH>> 3) Не осуществляется полный анализ всех возможных вариантов. Такой анализ вообще возможен только в случае, когда у нас есть нечто хотя бы напоминающее абстрактную* математическую модель, в противном случае количество вариантов будет слишком большим для такого анализа. Например, нужен анализ всех вариантов одновременных операций при доступе нескольких пользователей к иерархии ресурсов.

ZOI>Я бы сказал не хватает пункта 4 — нужно учитывать, что завтра могут поменяться требования и половину продукта придется перелопатить. Это очень печальный пункт, когда люди умудряются размазать логику по всем модулям, так что ее потом замучаешься вытаскивать

Пункт 4 здесь неуместен. Потому что каждый из предыдущих пунктов какбы намекает на решение проблемы.
А пункт 4 в применении к математической модели звучит так:
4': при добавлении в модель новой операции выяснилось, что эта операция не бьется с остальными, т.е. фактически разрушает текущую модель, и надо вместо нее придумывать новую.

Здравствуйте, DarkGray, Вы писали:

DG>зы
DG>не вижу пока, как ты именно через переход сеттеры -> геттеры уменьшаешь кол-во сущностей.

При сеттерном подходе если источник меняется из десяти мест, то и изменять состояние объектов зависящих от источника нужно тоже из десяти мест. При геттерном подходе при изменении источника изменять состояние зависящих объектов не нужно в принципе. Соответственно в коде на десять очень сложных сущностей стало меньше.

U>При сеттерном подходе если источник меняется из десяти мест, то и изменять состояние объектов зависящих от источника нужно тоже из десяти мест. При геттерном подходе при изменении источника изменять состояние зависящих объектов не нужно в принципе. Соответственно в коде на десять очень сложных сущностей стало меньше.

в первом приближении это может быть реализовано как:

this.X = new_X1;
this.Update_X_Dependencies();
[..]

this.X = new_X2;
this.Update_X_Dependencies();

и так десять раз.
дублирование десять раз this.Update_X_Dependencies() еще не похоже на увеличение кол-ва сущностей

Здравствуйте, DarkGray, Вы писали:

DG>и так десять раз.
DG>дублирование десять раз this.Update_X_Dependencies() еще не похоже на увеличение кол-ва сущностей

Это синтаксический сахар, от которого сущности никуда не делись. Как только, к примеру, окажется, что код изменяющий X не знает всех объектов, которые от X зависят, это станет очевидным.

Здравствуйте, DarkGray, Вы писали:

DG>и так десять раз.
DG>дублирование десять раз this.Update_X_Dependencies() еще не похоже на увеличение кол-ва сущностей

Т.е. в общем случае подход с явными апдейтами не работает, вместо него приходится использовать события. Соответственно в коде появляется столь сложная в понимании и опасная в примении сущность как события и подписка на них. В геттерном коде таких сущностей в принципе нет.

ZOI>>Я бы сказал не хватает пункта 4 — нужно учитывать, что завтра могут поменяться требования и половину продукта придется перелопатить. Это очень печальный пункт, когда люди умудряются размазать логику по всем модулям, так что ее потом замучаешься вытаскивать

HH>Пункт 4 здесь неуместен. Потому что каждый из предыдущих пунктов какбы намекает на решение проблемы.

если этот пункт переформулировать, то он становится уместным:
значительная часть ошибок вызвана тем, что в коде не записывается модель, а записывается лишь решение вытекающее из этой модели, а модель остается в голове разработчика, что:
во-первых: приводит к необходимости восстановления модели из кода при каждом изменении кода (со всеми проблемами из этого вытекающими),
во-вторых: делает невозможным применение автоматизированных средств для управления(верификация, преобразования и т.д.) моделью

Здравствуйте, Undying, Вы писали:

U>При сеттерном подходе если источник меняется из десяти мест, то и изменять состояние объектов зависящих от источника нужно тоже из десяти мест. При геттерном подходе при изменении источника изменять состояние зависящих объектов не нужно в принципе. Соответственно в коде на десять очень сложных сущностей стало меньше.

покажи пример кода при геттерном подходе

U> Соответственно в коде появляется столь сложная в понимании и опасная в примении сущность как события и подписка на них.

т.е. падает показатель предсказуемости кода?

о том и речь, что первичная задача — максимизировать предсказуемость, и используется корреляция, что при уменьшение кол-ва сущностей увеличивается предсказуемость (но в общем случае, уменьшение кол-ва сущностей не ведет к увеличению предсказуемости, а переход с push на pull может давать и увеличение кол-ва сущностей, особенно на стыке с внешним окружением: как минимум требуется писать синхронайзер под каждый класс из внешнего окружения)

M>покажи пример кода при геттерном подходе

в первом приближении можно считать, что это функциональный подход с поддержкой ленивости адаптированный под ООП

Здравствуйте, HrorH, Вы писали:

HH>Здравствуйте, Skynin, Вы писали:

HH>Я не знаю, как объяснить, потому что сам еще мало что понимаю.
Во втором и не сомневался. Потому что тогда знали бы как объяснить

HH>Я пишу программы в области документооборота. Вам стало легче?
Мне и не было тяжело. Это вы потроллиться что-ли предлагаете?

Лучше расскажите конкретней, как в своей области вы применяете математические методы

HH>Математика — это всего лишь язык, инструмент, которым можно пользоваться.
Разумеется. И как всякий инструмент его можно применять И неумело, И не к месту.

HH>Я порекомендовал модели, как одно из средств, которое позволяет избежать ошибок уже на этапе продумывания спецификации программы.
А я спросил — на чем основаны эти рекомендации? На каком успешном опыте?

Мало того, указал и на причины почему не только мне, а вообще такой успешный метод массово — неизвестен.

HH>Использовать ли их, и в каких случаев, это дело каждого.
О нет, я могу рекомендовать для написания надежных программ рисовать на стенах в офисе желтые квадраты в синий горошек.
"А использовать ли этот отличный метод — это дело каждого!"

HH>Я не собираюсь их навязывать.
А вы попытайтесь :D

Или хотя бы победите в конкурентной борьбе других разработчиков в области документооборота.

HH>Более того, я хотел бы узнать, какие вообще есть средства, чтобы минимизировать количество ошибок.
Минимальный набор, существующий в отрасли я указал.
Книг, исследований же на эту тему написано немало, как с анализом причин, причем разнообразных, не связанных между собой одной категорией,
так и с методиками уменьшения влияния этих причин на качество конечных программных продуктов.
Извините что так размыто "Формулы" у меня нет, и не встречал у кого она есть.
У вас вот тоже(просто "удивительно"!) тоже — "сам еще мало что понимаю"
Вот о том что Вы, и обычно увлеченные "математики" пока не понимают я и упомянул.

А Вы мне сразу о философии забросили. О нефальсифицируемости математики, как и религии с психологией, при одновременном их огромном значении и влиянии на человеческий интеллект, дух и душу, я рассуждаю на соответствующих форумах.

Здравствуйте, Константин, Вы писали:

vsb>>>Программы без ошибок появятся, когда появится искусственный интеллект.
VC>>ИИ не "появится", его создадут. И тоже с ошибками...
К>При этом способность совершать ошибки будет заложена в сам ИИ

Просто потому, что иначе не получится. ИИ не сможет ничего осознать, пока не сможет делать ошибок.

Здравствуйте, DarkGray,

Извини, не удержался.

U>> Соответственно в коде появляется столь сложная в понимании и опасная в примении сущность как события и подписка на них.

DG>т.е. падает показатель предсказуемости кода?

К чему это наукообразие? Показатель, функция, корреляция... Можно же выразиться проще: что становится трудно понять, как именно работает код и какие он вызывает побочные эффекты. Всё равно эти "показатели", "функции" и "корреляции" или вовсе нельзя рассчитать, или можно рассчитать только на очень ограниченном множестве переменных, которые не отражают всех факторов.

DG>о том и речь, что первичная задача — максимизировать предсказуемость, и используется корреляция, что при уменьшение кол-ва сущностей увеличивается предсказуемость (но в общем случае, уменьшение кол-ва сущностей не ведет к увеличению предсказуемости, а переход с push на pull может давать и увеличение кол-ва сущностей, особенно на стыке с внешним окружением: как минимум требуется писать синхронайзер под каждый класс из внешнего окружения)

Чтобы продраться через этот абзац пришлось прочесть всё сообщение сверху вниз, снизу вверх и ещё по диагонали. В контексте топика прекрасная иллюстрация того, как наукообразием можно замусорить даже самые простые сведения. По сути ты высказал простейшую мысль, что для реализации pull-модели могут понадобиться дополнительные интерфейсные объекты, но код будет проще читать, поскольку подписчики будут изолированы один от другого. В общем, обе мысли очевидны, но при чём тут "корреляция" и "предсказуемость" — тайна сия велика есть.

Здравствуйте, Skynin, Вы писали:

Попробую намекнуть на один из примеров, просто не хочется палиться.
Сразу станет понятно, что я понимаю слово "математический" несколько широко.
Даже в данном случае можно просто сказать — модель, не произнося слово математический.

Допустим у нас есть дерево объектов, и с этим деревом могут работать одновременно несколько пользователей.

В модели у нас должна быть операция редактирования объекта.
При этом объект должен блокироваться.

Также должна быть операция добавления нового объекта, удаления объекта, перемещения и копирования.

Возникает вопрос, какие блокировки и проверки нужны, чтобы все эти операции бились между собой, и пользователи не портили данных друг друга.
Ответом на этот вопрос и будет модель.
Здесь важно то, что при добавлении каждой новой операции в модель во всех остальных операциях это должно учитываться. Скажем, при добавлении операции удаления, при выполнении остальных операций должна добавиться проверка, что объект не удален.
При добавлении в систему безопасности, в операции редактирования добавляется проверка, есть ли права на редактирование, или только на чтение и т.д.
В операции удалении — что у нас есть права на удаление и т.д.
Тут есть куча подробностей, которые я приводить не буду, скажу только, что то, что я сейчас написал — не совсем корректно, и можно рассматривать только как иллюстрация.
А причем тут мат. модель? -спросите Вы.
Дело в том, что надо рассмотреть все попарные сочетания операций, и учесть все аспекты существующие в системе.
Это пока еще будет просто модель, она станет математической, когда и если появиться необходимость и возможность написать ее в соответсвующей нотации, ведь как я говорил, математика — это всего лишь язык.

Здравствуйте, HrorH, Вы писали:

HH>Более того, я хотел бы узнать, какие вообще есть средства, чтобы минимизировать количество ошибок.

Если уж смотришь в сторону функциональщины то смотри Зависимые типы и такие языки как например:

ATS http://www.ats-lang.org/ это более-менее практичный язык вполне годный для использования в прикладном программировании, но к сожалению еще далек от полноценного релиза.

Можешь также посмотреть Agda, Epigram, но это уже академично по моему.

Ну и если так сильно тянет в математику то посмотри еще Coq

Если же тебе нужны средства для более гражданских языков, то ищи по ключевым "контрактное программирование", "статический анализ".

Здравствуйте, FR, Вы писали:

Кое-что из этого уже пытался смотреть... Правда, пока мало что понял.
А чем помогут зависимые типы, если необходимо сделать корректную спецификацию программы?

DG>>т.е. падает показатель предсказуемости кода?

ГВ>К чему это наукообразие? Показатель, функция, корреляция...

пока задача не сформулирована через показатели, функции, корреляцию и т.д. — ее невозможно решить научным методом, а можно лишь решать методами тыка и взглядами в потолок.

ГВ>По сути ты высказал простейшую мысль, что для реализации pull-модели могут понадобиться дополнительные интерфейсные объекты, но код будет проще читать, поскольку подписчики будут изолированы один от другого.

что такое "проще читать"?

Здравствуйте, HrorH, Вы писали:

HH>Кое-что из этого уже пытался смотреть... Правда, пока мало что понял.
HH>А чем помогут зависимые типы, если необходимо сделать корректную спецификацию программы?

В этом мало помогут, это вообще неформализуемая задача, тут и математика ничем ни поможет.
Помогут в другом если уже формализация есть реализовать ее максимально безошибочно, конечно
помогут не только и не столько зависимые типы, а скажем весь арсенал что есть например в ATS.

Ну и тот же Coq вполне средство построения формальных моделей.

Ну и на фоне того что сама математика уже уперлась в пределы доказуемости я бы особо не надеялся
на то что это будет разрешимо для программирования.

Здравствуйте, FR, Вы писали:

FR>Здравствуйте, HrorH, Вы писали:

HH>>Кое-что из этого уже пытался смотреть... Правда, пока мало что понял.
HH>>А чем помогут зависимые типы, если необходимо сделать корректную спецификацию программы?

FR>В этом мало помогут, это вообще неформализуемая задача, тут и математика ничем ни поможет.

Я тут уже 2 раза в этой ветке приводил ссылку на то, как это сделано в FRP.
Вот другая ссылка, но из той же области
здесь

Люди как-то используют математику для написания спецификаций, а все мне говорят то про неформолизуемость, то про ограниченность самой математики...
Я не въезжаю, причем здесь ограниченность математики.
Почитайте бумаги Conal Elliott, если Вы их еще не читали. Вы то сможете это понять.
И не надо говорить, что это невозможно (неформализуемо), если это уже есть.

Здравствуйте, DarkGray, Вы писали:

DG>>>т.е. падает показатель предсказуемости кода?
ГВ>>К чему это наукообразие? Показатель, функция, корреляция...

DG>пока задача не сформулирована через показатели, функции, корреляцию и т.д. — ее невозможно решить научным методом, а можно лишь решать методами тыка и взглядами в потолок.

Сначала нужно показать саму функцию "предсказуемости".

ГВ>>По сути ты высказал простейшую мысль, что для реализации pull-модели могут понадобиться дополнительные интерфейсные объекты, но код будет проще читать, поскольку подписчики будут изолированы один от другого.

DG>что такое "проще читать"?

Молодец! Эту фразу вообще можно выкинуть. Останется: "для реализации pull-модели могут понадобиться дополнительные интерфейсные объекты, но подписчики будут изолированы один от другого". Смысл не поменялся.

Здравствуйте, HrorH, Вы писали:


FR>>В этом мало помогут, это вообще неформализуемая задача, тут и математика ничем ни поможет.

HH>Я тут уже 2 раза в этой ветке приводил ссылку на то, как это сделано в FRP.
HH>Вот другая ссылка, но из той же области
HH>здесь

Ссылки не помогут, такие читать целая работа, расскажи вкратце суть.
Что такое FRP я знаю, но не вижу какое отношение имеет к формализации. Это скорее один из
элементов или паттернов проектирования. С таким же успехом можно сказать что с помощью
скажем ОО или монад уже все формализовано.

HH>Люди как-то используют математику для написания спецификаций, а все мне говорят то про неформолизуемость, то про ограниченность самой математики...
HH>Я не въезжаю, причем здесь ограниченность математики.
HH>Почитайте бумаги Conal Elliott, если Вы их еще не читали. Вы то сможете это понять.
HH>И не надо говорить, что это невозможно (неформализуемо), если это уже есть.

Еще раз объясни вкратце.

DG>>пока задача не сформулирована через показатели, функции, корреляцию и т.д. — ее невозможно решить научным методом, а можно лишь решать методами тыка и взглядами в потолок.

ГВ>Сначала нужно показать саму функцию "предсказуемости".

Предсказуемость'(код K, требование T)=минимального вычислительная сложность алгоритма, который для кода K проверяет требование T.
Предсказуемость = 1/Предсказуемость';

вернемся к примеру который уже был:

for (uint i = items.Length - 1; i >= 0; --i)
{
  var item = items[i];
  //что-то делаем с item
}
 
foreach (var item in items.Reverse())
{
  //что-то делаем с item
}

для кода вида, как во втором примере, требование "незацикливаться" проверяется простым автоматом за O(кол-во операторов в программе), а чтобы проверить на зацикливание код вида, как в первом варианте, необходим алгоритм со сложностью близкой к O(2^кол-во операторов в программе)

зы
изолированность хороша тем, что при правильной изоляции функция предсказуемости выглядит как:
Предсказуемость'(код, требование)=Sum(Предсказуемость'(изолированная часть кода_i, требование))
для неизолированного кода функция ведет себя много хуже:
Предсказуемость'(код, требование)=Product(Предсказуемость'(неизолированная часть кода_i, требование))

FR>Ну и на фоне того что сама математика уже уперлась в пределы доказуемости я бы особо не надеялся
FR>на то что это будет разрешимо для программирования.

основная проблема, что математики хотят всегда точное решение. и в статье по ссылке подразумевается, что теории могут быть только точными. на практике же в большинстве задач достаточно теорий и решений, которые описывают и решают задачу с частичной потерей точности.

Здравствуйте, FR, Вы писали:


FR>Ссылки не помогут, такие читать целая работа, расскажи вкратце суть.
FR>Что такое FRP я знаю, но не вижу какое отношение имеет к формализации.

Вообще получится из разряда, "я не люблю Карузо?"- "А ты его слышал?"- "Нет, мне Рабинович напел."

Вольный пересказ, в основном вот этого здесь

Я так понял, что при разработке теории функционального реактивного программирования этому Conal Elliot в голову пришла идея.
Во-первых, надо говорить про денотационную семантику (это то что придумали в 1960)

Denotational semantics is a compositional style for precisely specifying
the meanings of languages, invented by Christopher Strachey
and Dana Scott in the 1960s (Scott and Strachey 1971; Stoy 1977).
The idea is to specify, for each syntactic category C,
 a mathematical model [C] of meanings, and
 a semantic function [.]C :: C -> [C].

Так, вот тут есть семантическая функция, которая сопоставляет синтаксису в коде его значения в модели (здравствуй, Рабинович).

Так вот, идея была в том, что могут быть законы, которые выполняются для этой семантической функции.

Вот обсуждение этого в блоге Вадлера здесь.
Кстати он там рекомендует посмотреть здесь

Вот эти 2 бумаги кажется основные.
Но меня поразило именно то, что все эти апликативные функторы, монады и т.д. использовались именно для определения семантики программы, а сама реализация по мере развития библиотеки делалась более эффективной, то есть использовались другие конкретные типы, но сама модель оставалась почти неизменной.
Боюсь, что от моего описания лучше не стало, т.к. мне самому в этом еще разбираться и разбираться, поэтому если сможете прочесть, лучше сами потом расскажете
В конце концов Вадлер на ерунду обращать внимание не стал бы

Здравствуйте, DarkGray, Вы писали:

DG>т.е. падает показатель предсказуемости кода?

Падает, но это одно из следствий. А нас интересует причина почему это происходит.

DG> а переход с push на pull может давать и увеличение кол-ва сущностей, особенно на стыке с внешним окружением

С чего это будет увеличение количества сущностей? В общем случае при геттерном подходе любой объект представляется в виде автоматического кэша с несколькими входами, в событийной — в виде объекта подписанного на несколько событий.

Проблемы событийного подхода:

1) Проблема лишних модификаций приемника. Если объект подписан на три события, то может возникнуть ситуация при которой одна логическая транзакция порождает три модификации приемника вместо одной. Причем первые две модификации происходят в невалидном состоянии системы, когда логическая транзакция отработала только частично.

2) Проблема оповещения о изменении инициатора изменений. Если объект подписанный на размер контрола, сам изменяет этот контрол, то контрол порождает событие и в этом объекте. Причем опять же вызов этого события происходит в невалидном состоянии системы, т.е. до завершения логической транзакции.

3) Каждый источник должен знать все объекты от него зависящие (пусть и в виде специализированного интерфейса). Соответственно возникает проблема отписки.

Все перечисленные проблемы обнаруживаются бритвой Оккама, т.е. порождают сущности, которых нет в логическом решении. В первом и втором виде проблем в виде лишних вызовов обработчиков событий в рантайме, в третьем — в виде записи в коде и вызовах в рантайме кода отписки от событий. При этом если в третьей проблеме порождаются просто дополнительные сущности, что еще полбеды, то в первой и второй проблемы — это сущности-вредители, которые не просто лишние, но еще и заставляют работать систему в невалидном состоянии, что и делает событийный код крайне сложным и трудно предсказуемым.

При этом если усложнять код, то для третьей проблемы есть неплохое решение, для второй проблемы — плохое, но работающее, но способа решить первую проблему я не вижу вовсе.

При геттерном подходе таких проблем нет в принципе.

Здравствуйте, HrorH, Вы писали:

HH> А что если предположить, что баг не должно быть вообще? Почему человек не может думать без ошибок?

Homo erratum est. вот поэтому.

Здравствуйте, HrorH, Вы писали:

HH>Здравствуйте, FR, Вы писали:

HH>при разработке теории функционального реактивного программирования этому Conal Elliot в голову пришла идея.
HH>Во-первых, надо говорить про денотационную семантику (это то что придумали в 1960)
HH>and Dana Scott in the 1960s (Scott and Strachey 1971; Stoy 1977).
Да-да, очень свежие идеи.
И конечно чистая случайность что они не выстрелили до сих пор

HH>Так, вот тут есть семантическая функция, которая сопоставляет синтаксису в коде его значения в модели.
Погуглил "рядом" с указанными источниками. Многовато речи идет о DSL. Вы уверены что DSL это "математика"?

HH>Так вот, идея была в том, что могут быть законы, которые выполняются для этой семантической функции.

HH>Вот обсуждение этого в блоге Вадлера
HH>Кстати он там рекомендует посмотреть

HH>Вот эти 2 бумаги кажется основные.
И посвящены языковым проблемам, а не проектированию и верификации ПО.

Посмотрел также CV Conal Elliott, потому что вобщем-то у вас он единственный свежий источник вдохновения.
То что сейчас он хаскелист ладно.
Смотрим что же привело его к этому, какая такая трудовая биография.
А там — сплошь графические алгоритмы, 2D, анимайтед 3D, вертексы с шейдерами из C# и проч.
То есть сама область — сугубая математика. То есть человек вырос на чисто математических задачах
Далее, вырос так что и начал заниматься "DSL" — Vertigo, a language and compiler for computations on graphics processors.
или: Pajama a compiler to produce highly optimized Java applets from simple, declarative specifications of interactive media (e.g., imagery, animation, sound).

HH>Но меня поразило именно то, что все эти апликативные функторы, монады и т.д. использовались именно для определения семантики программы, а сама реализация по мере развития библиотеки делалась более эффективной, то есть использовались другие конкретные типы, но сама модель оставалась почти неизменной.
А чего моделям с которыми работал Conal Elliott изменяться?
Такая у него предметная область — устойчивая.

HH>В конце концов Вадлер на ерунду обращать внимание не стал бы
Хорошо, читаем кто такой этот Вадлер:
Philip Wadler
Position: Professor
Roles: Member of Laboratory for Foundations of Computer Science
Research Interests: Programming languages, functional programming, type systems, web programming, query languages for databases, hybrid and gradual typing, Haskell, Erlang, Java, XML.

То есть "академик" и преподаватель, как понимаю с его емайла inf.ed.ac.uk.
Cугубо научная работа. С чистенькими, рафинированными проблемами.

Студентом у него думаю быть интересно и полезно. Да и вообще, укрепить некие фундаментальные знания.

Но вот в остальном оказался прав — у вас даже источники сплошь из высших сфер, или особых областей программирования.

Здравствуйте, monax, Вы писали:

U>>При сеттерном подходе если источник меняется из десяти мест, то и изменять состояние объектов зависящих от источника нужно тоже из десяти мест. При геттерном подходе при изменении источника изменять состояние зависящих объектов не нужно в принципе. Соответственно в коде на десять очень сложных сущностей стало меньше.

M>покажи пример кода при геттерном подходе

http://rsdn.static.corbina.ru/forum/design/3612218.1.aspx

U>С чего это будет увеличение количества сущностей? В общем случае при геттерном подходе любой объект представляется в виде автоматического кэша с несколькими входами, в событийной — в виде объекта подписанного на несколько событий.

ты опять про внутренние объекты, а я тебе про внешние объекты: БД, файловая система, UI, сеть и т.д., и взаимодействие с ними.

например, если есть набор объектов Button, то чтобы задействовать все поля Button-а через getter-ы необходимо добавить внутренний объект ButtonState + добавить class ButtonSynchronizer, который применяет ButtonState к Button.

U>Падает, но это одно из следствий. А нас интересует причина почему это происходит.

причина падения предсказуемости при событийном подходе в росте кол-ва трасс, которые необходимо рассмотреть, чтобы сделать тот или иной вывод.

Здравствуйте, DarkGray, Вы писали:

DG>причина падения предсказуемости при событийном подходе в росте кол-ва трасс, которые необходимо рассмотреть, чтобы сделать тот или иной вывод.

Причем подавляющее большинство этих трасс с точки зрения логики решения является чистым мусором, т.к. в логики решения таких трасс нет и близко. Соответственно событийный подход это способ превратить тривиальную задачу в монстрообразное решение.

Здравствуйте, DarkGray, Вы писали:

DG>ты опять про внутренние объекты, а я тебе про внешние объекты: БД, файловая система, UI, сеть и т.д., и взаимодействие с ними.

Там все то же самое только вместо автоматических кэшей используются LazyMaker'ы.

DG>например, если есть набор объектов Button, то чтобы задействовать все поля Button-а через getter-ы необходимо добавить внутренний объект ButtonState + добавить class ButtonSynchronizer, который применяет ButtonState к Button.

Зачем? Пишется LazyMaker зависящий от нужных входов, вызов LazyMaker.Make вставляется в OnPaint контрола, если входы изменились, то вызывается обработчик, изменяющий нужные свойства Button'а. Соответственно если какие-то изменения нам нужно немедленно отобразить пользователю, то достаточно после выполнения изменений выполнить перерисовку формы. Код UI становится примитивней паровоза, никакого сравнения с событийным кошмаром.

U>Зачем? Пишется LazyMaker зависящий от нужных входов, вызов LazyMaker.Make вставляется в OnPaint контрола, если входы изменились, то вызывается обработчик, изменяющий нужные свойства Button'а.

Т.е. никакой инкапсуляции? это возможно только для каких-то очень простых программ с отношениями только вида 1 к 1.
возьмем, например, графический редактор схем, состоящий из нескольких widget-ов: поле и список всех элементов.
допустим, что элементы подписываются и на поле, и в списке.
как тогда запишется правило, что название выделенного элемента должен выводится жирным зеленым шрифтом с размером на 10% больше умолчательного?

зы
в первом приближении, чтобы не было дублирования — это записывается или так (это будет Push):

void UpdateControl_ForSelectedElement(Control control)
{
  control.Font = new Font{Bold=true, Size = default.Font.Size * 1.1};
  control.Color = Colors.Green;
}

или так (pull):

ControlState ControlState_ForSelectedElement()
{
  return new ControlState
  {
    Font = new Font{Bold=true, Size = default.Font.Size * 1.1};
    Color = Colors.Green;
  };
}

или так (pull, в идеале):

ControlState ControlState_ForSelectedElement()
{
  return new ControlState
  {
    Font = new FontState{Bold=true, SizeK = 1.1};
    Color = Colors.Green;
  };
}

соответственно, и появляется <T>State и <T>Synchronizer для каждого внешнего class-а <T>

Здравствуйте, DarkGray, Вы писали:

U>>Зачем? Пишется LazyMaker зависящий от нужных входов, вызов LazyMaker.Make вставляется в OnPaint контрола, если входы изменились, то вызывается обработчик, изменяющий нужные свойства Button'а.

DG>Т.е. никакой инкапсуляции?

Причем здесь инкапсуляция и какие с ней могут быть проблемы?

DG>возьмем, например, графический редактор схем, состоящий из нескольких widget-ов: поле и список всех элементов.
DG>допустим, что элементы подписываются и на поле, и в списке.
DG>как тогда запишется правило, что название выделенного элемента должен выводится жирным зеленым шрифтом с размером на 10% больше умолчательного?

LazyMaker selectedElementMaker = new LazyMaker(delegate
  {
    selectedElement.Control.Font = new Font{Bold=true, Size = default.Font.Size * 1.1};
    selectedElement.Control.Color = Colors.Green;
  },
  delegate { return selectedElement; }
);

void OnPaint()
{
  selectedElementMaker.Make();
}

DG>соответственно, и появляется <T>State и <T>Synchronizer для каждого внешнего class-а <T>

Ты что такое LazyMaker понял? Синхронайзер это, конечно, хорошее решение по сравнению событиями, но так-то в силу своей активности это плохое решение. LazyMaker решает те же задачи, будучи пассивным. За счет чего и надежнее, и проще, и оптимальней по быстродействию.

U> Причем здесь инкапсуляция и какие с ней могут быть проблемы?

потому что тогда весь код, который отвечает за вывод элемента (а это могут быть тысячи строк кода, которые определяют как элемент выводится при тех или условиях, задачах, настройках и т.д.) — необходимо запихать в один LazyMaker

U> LazyMaker selectedElementMaker

тогда уж (если все-таки хочется инкапсуляцию)

LazyMaker selectedElementMaker = new LazyMaker(()=>UpdateControl_ForSelectedElement(selectedElement.Control),
 delegate { return selectedElement; }
);

это Push, и имеет характерные проблемы связанные с Push.
в частности, тяжело подмешивать декораторы, например, что элементы на поле должны выводится дополнительно Italic-ом,
а название элемента при наведении мышкой должен выводится синим (и это приоритетнее, чем вывод выделенности)

зы
фактически LazyMaker использует промежуточный подход:
push заменен на pull для отслеживания зависимостей между элементами, но сами данные push-атся

Здравствуйте, DarkGray, Вы писали:

DG>если этот пункт переформулировать, то он становится уместным:
DG>значительная часть ошибок вызвана тем, что в коде не записывается модель, а записывается лишь решение вытекающее из этой модели, а модель остается в голове разработчика, что:
DG>во-первых: приводит к необходимости восстановления модели из кода при каждом изменении кода (со всеми проблемами из этого вытекающими),
DG>во-вторых: делает невозможным применение автоматизированных средств для управления(верификация, преобразования и т.д.) моделью

Точные замечания.

И тут мы приходим к вопросу — а как поможет с рассогласованием модели запись ее в виде математических выражений?
Более обобщенно — какая "алфавитно"-символьная запись позволяет бороться с таким рассогласованием, и наоборот — позволяет быстро восстановить модель в уме человека?
Для компьютера такая запись всего лишь должна быть однозначной. А человеку это помогает слабо, при увеличении количества знаков описания будь то самой модели, или ее решений.

Из попытки решить эту проблему и появляются 2 подхода: DSL и метапрограммирование. Утрировано их суть — уменьшить количество знаков при описании, за счет увеличения их емкости, или вынесения описания контекста куда-то во вне.

Но это частичное решение.
Письменность, частным случаем которой и является запись на языке программирования есть и дар и бич человека.
Каждый программист знает что собственный код со временем читается ничуть не легче чем чужой.

И получается, что сохранить жесткое соответствие модели и кода на ЯП можно только запретив программисту править код. Собственно RAD, CASE системы и всякие генераторы у фреймворков и есть такая попытка.
Но "абстракции текут" и лезть в код приходится.

И какой же выход предлагают адепты ФП, хаскелей и "математики"?
На самом то деле ничего радикального. они предлагают то же самое что уже и так есть:
добиться восстановления модели из символьной записи, чтобы протестировать эту модель автоматизированными средствами.
Но восстановления — КЕМ? Человеком? А чем математическая запись проще в чтении чем код на ЯП? Например: Сколько времени понадобилось проверять доказательство Григория Перельмана? Или — почему Степанов на лекции в Яндексе говорил что наука построена на доверии, "у меня просто нет времени проверить даже 20ти страничное доказательство которое мне друг месяц тому дал почитать"

А если НЕ человеком, то хоть битами записывай 0110111001 — компьютер не устает и не ошибается при чтении.

Увлеченные "математикой" не понимают что внутри самой математики с записью, восстановлением и верификацией уже немалые проблемы.
Вернее — те же. Просто ошибки там выявляются по другому.

Что же до "доказательства верности программ", то я вообще слабо представляю, как математики, которые не решили проблемы, автоматического доказательства утверждений у себя, собираются помочь в этом программистам?
Где та методика у самих математиков — наваял Перельман доказательство — запихнули его в компьютер, или просто по листикам раздали студентам с "инструкцией выполнения" и опа — "доказательство верно!" или "доказательство неверно в такой строчке на такой-то странице!"

S>Более обобщенно — какая "алфавитно"-символьная запись позволяет бороться с таким рассогласованием, и наоборот — позволяет быстро восстановить модель в уме человека?

такая которая позволяет задачу восстановления модели поручить компьютеру.

Здравствуйте, HrorH, Вы писали:

HH> Мне кажется, основная причина в том, что разработка происходит стихийно, каждый пишет, что ему придет в голову.
HH> 1) Не формулируется математическая модель...

Всё ясно. Как уже правильно обобщил Carc, математик пытается умничать в области, где сам ниструя не понимает.
Программинг только на заре 70-ых был "академическим", да и то математика там привлекалась только в силу требуемых алгоритмов. В целом же, программинг — это вообще отдельная дисциплина, где не то что "математическую модель", пару квадратов на бумаге — и то сложно расположить! Простой пример: GUI usability. Психология+интуиция+чтобы работало. Или вот базы данных — их что, по рядам Фурье считают? Далеко нет. Тупо "на практике" проверяют, будет ли отзывчивой система при 20 запросах в сек. Почему 20? Да просто эмпирика!
Кроме того, сидеть и рисовать мат.абстракции — это и студент в туалете может, ты попробуй напиши то, чего ещё НИКОГДА НЕ БЫЛО! Ну типа как придумать свою теорему Ферма. Этим и занимаются настоящие профи — на базе опыта, статей, чутья, каких-то полуабстрактных моделей пытаются хотя бы набросать каркас будущей системы. Тут не математика, тут даже бубен сто крат полезнее!
А говносистемы получаются не от зла большого — просто не у всех есть нужный опыт и инженерное мышление. Но пробовать-то надо! Глядишь — вторая система будет намного лучше. Кстати, "говносистемы" как раз и получаются из-за того, что один говноархитектор всё придумал, пол-системы написали, а выкидывать и писать заново НА ОСНОВЕ ОПЫТА — не хотят (сроки/деньги и т.п. чушь). Был бы у каждой системы второй шанс — всё было бы намного лучше.

Здравствуйте, matumba, Вы писали:

M>Был бы у каждой системы второй шанс — всё было бы намного лучше.

Второго шанса может не понадобиться, если изначально закладывать в систему возможность ошибаться.

Здравствуйте, IT, Вы писали:

IT>Не вижу в твоём утверждении логической связи между тем, что после 'если' и после 'то'.

"Сложность", по определению, это количество ошибок на километр кода. Если мы рассматриваем программирование как управление количеством ошибок на километр кода то, согласно закону сохранения сложности, любая конструкция является ошибкой или ошибок вообще не бывает.

Здравствуйте, Ромашка, Вы писали:

IT>>Не вижу в твоём утверждении логической связи между тем, что после 'если' и после 'то'.
Р>"Сложность", по определению, это количество ошибок на километр кода.

Откуда такое "поопределение"?

Здравствуйте, IT, Вы писали:
Р>>"Сложность", по определению, это количество ошибок на километр кода.
IT>Откуда такое "поопределение"?

У тебя есть другое, которое не сводится к ошибкам на километр? Озвучь, пожалуйста.

Здравствуйте, Ромашка, Вы писали:

Р>>>"Сложность", по определению, это количество ошибок на километр кода.
IT>>Откуда такое "поопределение"?
Р>У тебя есть другое, которое не сводится к ошибкам на километр? Озвучь, пожалуйста.

Если коротко, то я это понимаю как меру усилий, требуемых для решения поставленной задачи.

Здравствуйте, DarkGray, Вы писали:

DG>потому что тогда весь код, который отвечает за вывод элемента (а это могут быть тысячи строк кода, которые определяют как элемент выводится при тех или условиях, задачах, настройках и т.д.) — необходимо запихать в один LazyMaker

Не понял проблемы. Если тебе по условию задачи нужно при изменении входа выполнить тысячи строк кода, то чем LazyMaker как место вызова этих тысяч строк кода хуже нежели любое другое? Никаких дополнительных ограничений на эти тысячи строк кода LazyMaker не накладывает, т.е. эти тысячи строк можно структурировать каким угодно образом, хоть объектным, хоть любым другим.

DG>тогда уж (если все-таки хочется инкапсуляцию)
DG>

DG>LazyMaker selectedElementMaker = new LazyMaker(()=>UpdateControl_ForSelectedElement(selectedElement.Control),
DG> delegate { return selectedElement; }
DG>);
DG>

Не вижу здесь никакой дополнительной инкапсуляции. Что изменилось-то от того, что ты код обработки вынес из LazyMaker'а в функцию этого же контрола?

DG>это Push, и имеет характерные проблемы связанные с Push.

Естественно Push. Каким это чудом у тебя на стыке с сеттерным кодом может быть Pull?

DG>в частности, тяжело подмешивать декораторы, например, что элементы на поле должны выводится дополнительно Italic-ом,
DG>а название элемента при наведении мышкой должен выводится синим (и это приоритетнее, чем вывод выделенности)

Не вижу проблемы. Сложность определяется исключительно логической сложностью задачи, никакой дополнительной сложности LazyMaker не вносит.

Здравствуйте, Skynin, Вы писали:

S>Что же до "доказательства верности программ", то я вообще слабо представляю, как математики, которые не решили проблемы, автоматического доказательства утверждений у себя, собираются помочь в этом программистам?

Очень просто, в программах большинство инвариантов, требующих доказательства, сводятся к примитивной арифметике и логике первого порядка, там автоматизированная проверка не представляет такой уж большой проблемы. Делая очередную опердень, теорему Гёделя не получишь. Кое-какие примеры на ATS я показывал тут, например реализация хитрой сортировки с машинно-проверенным доказательством того, что результат действительно отсортирован для любых входных данных, и что при работе с массивом 100% не будет выходов за его пределы (без рантайм-проверок!).

S>Где та методика у самих математиков — наваял Перельман доказательство — запихнули его в компьютер, или просто по листикам раздали студентам с "инструкцией выполнения" и опа — "доказательство верно!" или "доказательство неверно в такой строчке на такой-то странице!"

Она есть — автоматические "доказатели теорем" вроде Coq. Как раз Coq последнее время все больше используется для автоматизированного доказательства и проверки новых теорем. Некоторые из них такие большие, что без него, вручную, доказать их просто не вышло бы.

Здравствуйте, DarkGray, Вы писали:

S>>Более обобщенно — какая "алфавитно"-символьная запись позволяет бороться с таким рассогласованием, и наоборот — позволяет быстро восстановить модель в уме человека?

DG>такая которая позволяет задачу восстановления модели поручить компьютеру.

Епть, так язык программирования и есть такая запись
Почитайте определение языка программирования хотя бы в википедии.

Проблема в авторе — создавшем модель, записавшем ее.

Здравствуйте, D. Mon, Вы писали:

DM>Очень просто, в программах большинство инвариантов, требующих доказательства, сводятся к примитивной арифметике и логике первого порядка, там автоматизированная проверка не представляет такой уж большой проблемы.
Ну раз очень просто — ждем-с.
Мне в начале 90ых усиленно доказывали что лет через 10 программисты вообще не будут нужны. Но может пару тысяч на все человечество.

DM>результат действительно отсортирован для любых входных данных, и что при работе с массивом 100% не будет выходов за его пределы (без рантайм-проверок!).
Да-а-а-а, Достижение!

DM>Она есть — автоматические "доказатели теорем" вроде Coq. Как раз Coq последнее время все больше используется для автоматизированного доказательства и проверки новых теорем.
Очередная сказочка. Coq утрировано говоря — это типизированный Prolog. Со всеми вытекающими.

P.S.
DM>Она есть — автоматические "доказатели теорем" вроде Coq. Как раз Coq последнее время все больше используется для автоматизированного доказательства и проверки новых теорем.

Не мое, но совсем не удивлен:
Coq — очень мошная система, и пожалуй мой любимый язык программирования, на данный момент.
...
Одна из дилемм: либо надо писать громоздкие предикаты, и ломать глазки. Либо написать покомпактнее, но автоматизация начинает спотыкаться. И опять-таки надо ломать глазки об многобукв. Хотя там много простейших шагов, который давно научились автоматизировать. А вот вместе все пока не очень складывается.

Все это опять-таки преодолимо, но геморрно. На промышленное применение ИМХО не тянет.
Про Coq

Вообще, когда вместо обсуждения проблемы, аргументов и контр-аргументов используется обмен именами, перед которыми нужно падать ниц — это несерьезно.

Здравствуйте, Skynin, Вы писали:

DM>>Очень просто, в программах большинство инвариантов, требующих доказательства, сводятся к примитивной арифметике и логике первого порядка, там автоматизированная проверка не представляет такой уж большой проблемы.
S>Ну раз очень просто — ждем-с.

А чего ждать — бери да используй. Нужные языки и инструменты уже появляются. Вон, Кармак вовсю нахваливает статический анализ кода, в том числе появившийся в полной версии VS10, — это все из той же оперы.

S>Мне в начале 90ых усиленно доказывали что лет через 10 программисты вообще не будут нужны. Но может пару тысяч на все человечество.

Ну это понятно, что глупость.

DM>>результат действительно отсортирован для любых входных данных, и что при работе с массивом 100% не будет выходов за его пределы (без рантайм-проверок!).
S>Да-а-а-а, Достижение!

Вообще-то да. Гарантия остутствия багов при сохранении эффективности — хорошая вещь. А большинство алгоритмов в современном софте не сложнее той сортировки. По той ссылке у меня есть и более практичный пример с фильтрацией IP адресов. Там машинные доказательства используются при работе с файлами и памятью, программа с багами по этой части просто не компилируется. Это определенно достижение.

DM>>Она есть — автоматические "доказатели теорем" вроде Coq. Как раз Coq последнее время все больше используется для автоматизированного доказательства и проверки новых теорем.
S>Очередная сказочка. Coq утрировано говоря — это типизированный Prolog. Со всеми вытекающими.

Почему сказочка? Вон теорема о 4 красках была доказана только благодаря применению компьютера, а окончательно в ней убедились после формализации на Coq. Многие разделы математики сейчас активно формализуются на нем, т.е. сами математики его активно используют.

Здравствуйте, Skynin, Вы писали:

S>Вообще, когда вместо обсуждения проблемы, аргументов и контр-аргументов используется обмен именами, перед которыми нужно падать ниц — это несерьезно.

Это имена не для падания ниц, а ссылки на современную практику. Но если угодно ее отрицать, то можете падать ниц, пожалуйста.

Здравствуйте, D. Mon, Вы писали:

DM>Это имена не для падания ниц, а ссылки на современную практику. Но если угодно ее отрицать, то можете падать ниц, пожалуйста.
Это не современная практика программирования, а научные, лабораторные изыскания.
Даже хаскель НЕ современная практика, а вы уже Coq туда записали? И какие у него достижения, смогли на нем записать "перебор" карт для решения теоремы о 4ех красках?

А ниц как раз фаны падают. Ничего на самом деле не имею ни против хаскеля ни против Coq. Есть проблемы, и народ ищет способы их решения.
Думаете я в первый раз задаю вам вопросы о проблематике? В ответ ни рассуждений, ни опровержений а ссылки на "божьи имена".
Но ощущение нередко — что фаны эти вообще не программисты. Говорим как о напрочь несвязанной профессиональной проблематике.

Здравствуйте, D. Mon, Вы писали:

DM>А чего ждать — бери да используй. Нужные языки и инструменты уже появляются.
Так бери и используй. Я тогда не понял ни откуда взялась эта тема, ни откуда вообще такая мировая проблема.

DM>Вон, Кармак вовсю нахваливает статический анализ кода, в том числе появившийся в полной версии VS10, — это все из той же оперы.
И что? Что с очередным движком у Кармака то приключилось?
Я о — нахваливает — а результат какой?

S>>Да-а-а-а, Достижение!
DM>Вообще-то да. Гарантия остутствия багов при сохранении эффективности — хорошая вещь.
Вы не поняли. Мы в 21ом веке наконец то научились тестировать сортировку и проверять выход за рамки массива.

DM>А большинство алгоритмов в современном софте не сложнее той сортировки.
Проблема в том что они часто вообще "не алгоритмы", а наборы произвольных правил, в отличие от сортировки.

DM>По той ссылке у меня есть и более практичный пример с фильтрацией IP адресов. Там машинные доказательства используются при работе с файлами и памятью, программа с багами по этой части просто не компилируется. Это определенно достижение.
Не спорю, задача частая и важная.

Только уж очень простая И конечно, это тоже достижение — наконец то ее решать с помощью машинных доказательств.

DM>Почему сказочка? Вон теорема о 4 красках была доказана только благодаря применению компьютера, а окончательно в ней убедились после формализации на Coq.
Потому что "тупой" перебор — известен давно.
То что записать наконец удалось математикам, освоить компьютер более грамотно — что ж

DM> Многие разделы математики сейчас активно формализуются на нем, т.е. сами математики его активно используют.
Ссылок на стастику не с сайта о Coq не будет я так понимаю?
Но даже если так, я рад за математиков.
Только нам программистам толку с этого мало, потому что есть кардинальные отличия.

Чтобы не повторятся, всего лишь одно назову: Проблема остановки.
Жду от "математиков" инструмента для устранения этого бага

Здравствуйте, Skynin, Вы писали:

DM>>Это имена не для падания ниц, а ссылки на современную практику. Но если угодно ее отрицать, то можете падать ниц, пожалуйста.
S>Это не современная практика программирования, а научные, лабораторные изыскания.

Так я именно про научные и отвечал — на вопрос "Где та методика у самих математиков — наваял Перельман доказательство — запихнули его в компьютер..."

S>Даже хаскель НЕ современная практика, а вы уже Coq туда записали? И какие у него достижения, смогли на нем записать "перебор" карт для решения теоремы о 4ех красках?

Ну вот математики чего-то формализуют, доказывают на нем:
http://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projects

S>Думаете я в первый раз задаю вам вопросы о проблематике? В ответ ни рассуждений, ни опровержений а ссылки на "божьи имена".
S>Но ощущение нередко — что фаны эти вообще не программисты. Говорим как о напрочь несвязанной профессиональной проблематике.

Вы задали вопрос "где та методика", я дал конкретный ответ — "вот". Какие рассуждения вам нужны?
Задали вопрос "как математики ... собираются помочь в этом программистам?", я дал конкретный ответ — например, вот так. А теперь делитесь странными эмоциями и обзываетесь. Некрасиво.

Здравствуйте, Skynin, Вы писали:

S>Даже хаскель НЕ современная практика, а вы уже Coq туда записали? И какие у него достижения

Например,
CompCert is a formally verified optimizing compiler for a subset of the C programming language which currently targets PowerPC, ARM and 32-bit x86 architectures. ... The compiler is specified, programmed and proved in Coq.

Здравствуйте, Skynin, Вы писали:

DM>>Вон, Кармак вовсю нахваливает статический анализ кода, в том числе появившийся в полной версии VS10, — это все из той же оперы.
S>И что? Что с очередным движком у Кармака то приключилось?

А что приключилось? Я не в курсе.
Вообще, их игры весьма стабильны были, и по его словам с применением статического анализа багов стало еще меньше.

S>Вы не поняли. Мы в 21ом веке наконец то научились тестировать сортировку и проверять выход за рамки массива.

А вы хотели чуда? Я вот в 26-м веке живу и рад, что смог ту сортировку доказать, а на ее примере поучиться доказательному программированию. Все лучше, чем писать сто тыщ тестов, которые все равно баги пропускают.

DM>>А большинство алгоритмов в современном софте не сложнее той сортировки.
S>Проблема в том что они часто вообще "не алгоритмы", а наборы произвольных правил, в отличие от сортировки.

Ну так и их можно теми же средствами формализовывать. Просто пока этим мало кто занимается, т.к. не умеют, не обучены и учиться не спешат.

DM>>По той ссылке у меня есть и более практичный пример с фильтрацией IP адресов. Там машинные доказательства используются при работе с файлами и памятью, программа с багами по этой части просто не компилируется. Это определенно достижение.
S>Не спорю, задача частая и важная.
S>Только уж очень простая И конечно, это тоже достижение — наконец то ее решать с помощью машинных доказательств.

Ну да, это ж учебный пример у меня.

S>Чтобы не повторятся, всего лишь одно назову: Проблема остановки.
S>Жду от "математиков" инструмента для устранения этого бага

В моем примере про IP адреса такой инструмент упоминается — termination metric. B ATS можно для рекурсивных функций и циклов формально доказать их завершимость, причем от программиста это требует минимум усилий. Это не решение той сугубо теоретической проблемы про определение завершимости произвольного алгоритма, это решение для повседневных практических задач — удостовериться, что мой код не виснет.

Здравствуйте, Skynin, Вы писали:

DM>>Вообще-то да. Гарантия остутствия багов при сохранении эффективности — хорошая вещь.
S>Вы не поняли. Мы в 21ом веке наконец то научились тестировать сортировку и проверять выход за рамки массива.

Тут принципиальный момент в том, что именно не "тестировать сортировку и проверять выход за рамки массива", а доказывать математически, да так, что доказательство проверяет машина, которая ничего не упустит. Т.е. степень уверенности в корректности совсем другая. И за счет такого доказательства можно убрать рантайм-проверки при работе с массивом, т.е. эффективность самой программы повышается. Раньше мы или полагались на внимательность программиста (и все знают, насколько это ненадежно), либо на рантайм-проверки в "безопасных" языках (и все знают, насколько это неэффективно).

Здравствуйте, D. Mon, Вы писали:

DM>Вы задали вопрос "где та методика", я дал конкретный ответ — "вот". Какие рассуждения вам нужны?
DM>Задали вопрос "как математики ... собираются помочь в этом программистам?", я дал конкретный ответ — например, вот
Спасибо, почитаю. Первые ж абзацы указывают что математики там не будет.

Поясню чем мне не нравятся ответы "математиков" — я задаю вопросы о "соленом", а ответы дают о "красном".
А истоки такого недоразумения выкристолизованы давно:
одни считают программирование подразделом математики, а другие, в частности я, видом "лингвистики".
Правда конечно где-то "посредине", но "математики" выбирают для доказательства успешности одни задачи, а "лингвисты" — другие
И одно дело когда "математиками" выбираются хорошо формализуемые задачи типа 3D да криптографии.
Но чаще, ввиду и ограничения форумного формата общения, простые, совсем низкого уровня абстракции.
Даже по Вашей ссылке, Вы рассматриваете "список с длинной", а в жизни то, которую приходится записывать на ЯП:
... при отгрузке товара Х движение по бухгалтерскому счету Y ...

Так вот и мой вопрос не о контроле границ массива. это для меня, программиста, давно неактуально.
Как и список с длиной. Как и верификация алгоритма сортировки и прочие мелочи, которые уже написаны, или которыми занимается весьма небольшое число людей.
А как математики ... собираются помочь в записи правил для гораздо более сложных сущностей программистам?
Я уж промолчу о затронутой проблеме соответствия моделей коду. Это уже пусть архитекторы систем допытываются

Здравствуйте, D. Mon, Вы писали:

S>>И что? Что с очередным движком у Кармака то приключилось?
Да так, с Rage проблемки мелкие.

Но Кармак конечно глыба, однозначно
Просто не он один пишет успешные движки для игр.
То есть применяемые им инструменты НЕ дают явного преимущества.

DM>А вы хотели чуда?
Зачем же чуда. Просто хороших примеров.

DM>рад, что смог ту сортировку доказать, а на ее примере поучиться доказательному программированию.
Ну если вы до сих пор пишите сортировки, то да, разделяю вашу радость

Я давно уж их не пишу, поэтому меня ваша радость не греет.

DM>Ну так и их можно теми же средствами формализовывать. Просто пока этим мало кто занимается, т.к. не умеют, не обучены и учиться не спешат.
Ну это понятно, люди во всем виноваты. Пишут программы, корабли в космос запускают (хотя математики ни асилили задачу о 3ех телах, а сжульничали), но вот они не умеют, не обучены и т.д.

Обычный аргумент хаскелистов — вот если б были не быдлокодерами, то освоили б, и было бы великое счастье

DM>Ну да, это ж учебный пример у меня.
Да я понимаю что в короткой заметке и не получится рассказать о другом.
Но уровень абстракции, вот в чем заковыка.
Открываем такого же количества буков разъяснение какого-нить паттерна ООП и сравниваем.

Утрировано говоря — вы приводите пример о фичах ассемблера.

S>>Чтобы не повторятся, всего лишь одно назову: Проблема остановки.
S>>Жду от "математиков" инструмента для устранения этого бага

DM>B ATS можно для рекурсивных функций и циклов формально доказать их завершимость, причем от программиста это требует минимум усилий.
...подключил нужную либу да и все.

DM>это решение для повседневных практических задач — удостовериться, что мой код не виснет.
Я не решаю подобные задачи на практике. Вернее я просто не замечаю когда решаю задачи подобного уровня.
Как не замечаю как завязываю шнурки на ботинках.

Здравствуйте, Skynin, Вы писали:

S>Спасибо, почитаю. Первые ж абзацы указывают что математики там не будет.

Она там есть, простая — арифметика да логика.

S>одни считают программирование подразделом математики, а другие, в частности я, видом "лингвистики".

Я не вижу противоречия между лингвистикой и математикой. Лингвистика математизируема, а математика, сама будучи языком, может быть предметом лингвистики.

S>Даже по Вашей ссылке, Вы рассматриваете "список с длинной", а в жизни то, которую приходится записывать на ЯП:
S>... при отгрузке товара Х движение по бухгалтерскому счету Y ...

Ну мы же умудряемся это записать в терминах 1С, SQL или C#. И списки, и отгрузку товара. И если списки можно формализовать и что-то про них доказать, то и отгрузку товара можно. Просто правил будет больше.

S>Так вот и мой вопрос не о контроле границ массива. это для меня, программиста, давно неактуально.

Для вас неактуально, а для тысяч программистов, в коде которых нашли тысячи уязвимостей с переполнением буфера, еще как актуально.

S>Как и список с длиной. Как и верификация алгоритма сортировки и прочие мелочи, которые уже написаны, или которыми занимается весьма небольшое число людей.
S>А как математики ... собираются помочь в записи правил для гораздо более сложных сущностей программистам?

Пока что ровно так же. Сортировка — это лишь пример, движение денег по счету не качественно сложнее, лишь количественно — числом правил. Но чем хорош подход компьютеризированного доказательства — компьютеру несложно проверить и 100 и 10000 правил, в то время как человек на таких объемах уже пасует, лепя баг за багом.

Здравствуйте, HrorH, Вы писали:

HH> Программирование — еще молодая область, возможно лет через сто появится нормальная методология разработки, которая позволит человеку не совершать ошибок...

HH>*Под абстракцией понимается выделение существенного.

Вспомнилось!
Ощущения от подобных дебатов, у меня как от истории:
Какой-то математик решил прочесть лекцию об эффективных способах раскроя ткани.
Пришло немало портных и их представителей.
Но после фразы, с которой он начал лекцию:
— Представим что человек это правильная сфера ...
бОльшая часть зала встала и ушла.

Я программист.
Ушел

Здравствуйте, Skynin, Вы писали:

S>Да так, с Rage проблемки мелкие.
S>То есть применяемые им инструменты НЕ дают явного преимущества.

Я бы по мелким проблемкам не спешил с такими выводами. А сколько движков было начато и недописано? Сколько дописано, но ценой многократно больших усилий? И вообще, много ли движков превзошли кармаковские? Обычно все только догоняли.

DM>>рад, что смог ту сортировку доказать, а на ее примере поучиться доказательному программированию.
S>Ну если вы до сих пор пишите сортировки, то да, разделяю вашу радость

Я часто занимаюсь довольно низкоуровневыми вещами — кодеки, обработка видео. Это не сортировки, но навыки нужны похожие.

S>Обычный аргумент хаскелистов — вот если б были не быдлокодерами, то освоили б, и было бы великое счастье

И чем он плох? Вы же не хотите, например, чтобы машины проектировали и собирали неграмотные быдлоинженеры и криворукие быдлосборщики. И чтоб стригли вас быдлопарикмахеры, и т.д. Но почему-то хотите, чтобы неграмотные программисты писали без багов. Это я называю желанием чуда.

DM>>B ATS можно для рекурсивных функций и циклов формально доказать их завершимость, причем от программиста это требует минимум усилий.
S>...подключил нужную либу да и все.

Нет, без либ. Дописал в сигнатуре функции выражение вроде .<a-b>. и все.

DM>>это решение для повседневных практических задач — удостовериться, что мой код не виснет.
S>Я не решаю подобные задачи на практике. Вернее я просто не замечаю когда решаю задачи подобного уровня.
S>Как не замечаю как завязываю шнурки на ботинках.

И не замечаете, как вносите баг за багом. Так все делают. А потом переделавают. И тестируют. И опять переделывают. Вместо того, чтобы один раз написать формализованно и дать компилятору проверить отсутствие противоречий.

Здравствуйте, matumba, Вы писали:

M>Здравствуйте, HrorH, Вы писали:

M>Всё ясно. Как уже правильно обобщил Carc, математик пытается умничать в области, где сам ниструя не понимает.
M>Программинг только на заре 70-ых был "академическим", да и то математика там привлекалась только в силу требуемых алгоритмов. В целом же, программинг — это вообще отдельная дисциплина, где не то что "математическую модель", пару квадратов на бумаге — и то сложно расположить! Простой пример: GUI usability. Психология+интуиция+чтобы работало. Или вот базы данных — их что, по рядам Фурье считают? Далеко нет. Тупо "на практике" проверяют, будет ли отзывчивой система при 20 запросах в сек. Почему 20? Да просто эмпирика!

Дальше поскипано...
Не стоит делать преждевременные выводы при таком недостатке информации.
Это наиболее частая и фатальная ошибка,
когда человек считает,
что он знает достаточно
для принятия решения о том,
чтобы не продолжать исследование дальше.

Вообщем Вы не угадали. И по поводу меня, и поводу применимости математики к базам данных.
И не обижайте меня, пожалуйста.
Если написал непонятно, то извините. В этой ветке есть еще мои комментарии, может помогут.

Здравствуйте, HrorH, Вы писали:

HH>Вообщем Вы не угадали. И по поводу меня, и поводу применимости математики к базам данных.

Если у вас в руках цифры — это ещё далеко не "математика". Ну а для интереса, можете щегольнуть каким-нибудь мат.аппаратом, который необходимо применяют в построении СУБД. Слушаем?...

Кратко, моя речь сводилась к тому, что программинг (особ. промышленный) отстоит от математики не ближе филателии или строительной инженерии.
Если в паре мест вам удалось "математически" доказать какой-то алгоритм, остыньте — не стоит обольщаться, что сейчас набегут математики и всю программную инженерию поставят на уши своими теоремами.
Программинг — это наука + искусство + интуиция. Причём "наука" в большей степени "логика".

Здравствуйте, matumba, Вы писали:

M>Здравствуйте, HrorH, Вы писали:

HH>>Вообщем Вы не угадали. И по поводу меня, и поводу применимости математики к базам данных.

M>Если у вас в руках цифры — это ещё далеко не "математика". Ну а для интереса, можете щегольнуть каким-нибудь мат.аппаратом, который необходимо применяют в построении СУБД. Слушаем?...

Во-первых, я не очень понимаю, что Вы подразумеваете под построением СУБД. Месье делает свой аналог Sql Server?
Мы сами-то Sql Server не строим, мы только юзаем.
Те кто строят, так там математики навалом. Причем разной.
Реляционная алгебра. Теория категорий. Что из этого используют для написания Sql Server — это вопрос к разработчикам.


M>Кратко, моя речь сводилась к тому, что программинг (особ. промышленный) отстоит от математики не ближе филателии или строительной инженерии.
M>Если в паре мест вам удалось "математически" доказать какой-то алгоритм, остыньте — не стоит обольщаться, что сейчас набегут математики и всю программную инженерию поставят на уши своими теоремами.
M>Программинг — это наука + искусство + интуиция. Причём "наука" в большей степени "логика".

Согласен.
Блин, это я сам виноват. Когда я написал математическая модель, то ударение надо было ставить не на слово математический, а на слово модель.
Что касается доказательств, то они также нужны не всегда. И вообще, слово математика я понимаю достаточно широко, как некий язык, на котором можно записывать свои мысли.
Да, действительно мне в нескольких местах удалось не то чтобы доказать алгоритм, а создать модель, которая помогла мне находить ошибки при разработке (в том числе в одном месте дело было связано с базой данных, я использовал теорию множеств).
Именно что для каждого случая модель нужно придумывать разную, подходящую для данной конкретной задачи.
В конце концов, многие используют в программе конечные автоматы, и это часто приводит к повышению надежности. Это ведь тоже математика.

S>Епть, так язык программирования и есть такая запись
S>Почитайте определение языка программирования хотя бы в википедии.

от того, что на ЯП в теории можно записать модель — совсем не означает, что сейчас на ЯП эти самые модели записываются.

например, от записи

class Segment
{
  public double Left;
  public double Right;
  public double Top;
  public double Bottom;
}

до модели отрезка — как отсюда до центра вселенной.

в данном случае, введение класса с такими полями это есть частное решение модели (вывод из модели), которая крутится у нас в голове:
1. всякий отрезок представим четырьмя координатами на плоскости
2. в декартовой системе координат можно ввести понятия лево-право(которые изоморфны отношению меньше-больше по оси X), вверх-вниз (которые изоморфны меньше-больше для системы координат принятой обычно в программировании, или больше-меньше принятой обычно в математике)
из этого, в частности, вытекает — что использование названии для полей Left/Right, Top/Bottom отчасти подразумевает, что для класса Segment используется инвариант: Top <= Bottom (или наоборот — в зависимости от выбранной системы координат), Left <= Right

и данный класс является именно частным решение модели (а не общим), потому что для отрезка четыре координаты могут браться произвольные: можно брать, например, центр отрезка и радиус-вектор, или конец отрезка, угол и длину и т.д.
задаваться отрезок тоже может сотней способов: в частности, например, как пересечение двух окружностей и т.д.

U> то чем LazyMaker как место вызова этих тысяч строк кода хуже нежели любое другое?

вот эти тысячи строк будут разделены на функции. Сигнатура этих функций будет push или pull?

U>Не вижу здесь никакой дополнительной инкапсуляции.

дай тогда определение инкапсуляции

U> Что изменилось-то от того, что ты код обработки вынес из LazyMaker'а в функцию этого же контрола?

где ты там увидел, что функция у самого же контрола?


DG>>это Push, и имеет характерные проблемы связанные с Push.

U>Естественно Push. Каким это чудом у тебя на стыке с сеттерным кодом может быть Pull?

какое отношение проблемы стыка имеют к способу задания правил вывода элемента?

Здравствуйте, DarkGray, Вы писали:

DG>для кода вида, как во втором примере, требование "незацикливаться" проверяется простым автоматом за O(кол-во операторов в программе), а чтобы проверить на зацикливание код вида, как в первом варианте, необходим алгоритм со сложностью близкой к O(2^кол-во операторов в программе)

Несколько озадачен: если тела циклов одинаковы, то откуда берётся O(2^N) при использовании for? ИМХО, различие будет только на сложность доказательства корректности for/foreach (если индекс неизменен в цикле). Ну, возможно, ещё добавится O(N), то есть по сути возвращаемся к тому же исходному O(N), если предположить, что в каждой строке тела цикла есть обращение к индексной переменной — нужно доказать, что эти обращения не изменяют индекс. Но двойка в степени N...

DG>зы
DG>изолированность хороша тем, что при правильной изоляции функция предсказуемости выглядит как:
DG>Предсказуемость'(код, требование)=Sum(Предсказуемость'(изолированная часть кода_i, требование))
DG>для неизолированного кода функция ведет себя много хуже:
DG>Предсказуемость'(код, требование)=Product(Предсказуемость'(неизолированная часть кода_i, требование))

В целом понятно, только всё равно, ИМХО, сформулировано запредельно громоздко. Нет, сказать по-простому: 1/вычислительная сложность проверки требования. А если вместо "проверки требования T" написать "доказательство свойства P", то получится ещё проще: "1/вычислительная сложность доказательства свойства P". Путаница возникает из-за того, что тривиальное значение слова "предсказуемость" не слишком похоже на твоё определение: интуитивно "предсказуемость" чаще понимается как сама возможность что-либо предсказать, вне количественных оценок сложности предсказания. Хотя соглашусь, что это тоже не бесспорно.