Тесты, которые тестируют тесты

Или почему в них нет необходимости.

Часто, когда рассказываешь новичкам про автоматическое тестирование, всплывает один и тот же вопрос: «А кто будет проверять сами тесты? Придётся писать тесты для тестов, потом тесты для тестов для тестов…» Все любят рекурсию и ещё больше любят уесть ей собеседника.

Странно, ни разу не попадался вопрос: «Кто тестирует тестировщиков?» — по сути, та же проблема вид сбоку.

Но действительно, почему нет необходимости тестировать тесты? (и тестировщиков)

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

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

Следующая схема должна пояснить мысль.

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

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

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

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

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

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

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

Поэтому я предпочитаю разработку длинными заходами:

  1. проектирование части одной модели (любой);
  2. реализация спроектированного;
  3. проектирование аналогичной части второй модели;
  4. реализация спроектированного;

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

На самом деле можно выделить не две, а три модели предметной области:

  • модель в коде функциональности;
  • модель в коде тестов;
  • модель в голове разработчика.

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

Во время работы над статьёй ни один тест не пострадал. Спасибо за внимание.
Метки:
Поделиться публикацией
Комментарии 170
  • +10
    Из этого так же вытекает, что тексты удваивают объём работы. Это в лучшем случае, не считая кода верификатора и ритуальных пританцовываний вокруг.
    • +17
      Увеличивают, но меньше чем в два раза. По моему опыту раза в 1.5. Бонусом идёт смещение времени обнаружения ошибок ближе ко времени реализации, что выливается в существенной экономии времени, особенно с ростом проекта.
      • +9
        Особенно это помогает, когда в проекте появляются новые люди.
        • +12
          И тут стоит вспомнить SQLite, где тестов в 1017 раз больше, чем кода=) Конечно, скорее исключение, но все же.
          • 0
            Я кстати заметил, что чем дальше развивается основной проект, тем кода становится меньше. Не потому что убиваются фичи, а скорей потому что происходит оптимизация микро и макро архитектуры под данные и реальную работу. А тесты себе как ходили так и ходят зеленые.

            Это очень помогает, когда сжимаешь код в 3-4 раза и потом запускаешь тесты. Вот тут вся польза тестов и видна.
        • +3
          В среднем случае это зависит от того, насколько тщательно писать тесты. По моему опыту — да, время на разработку небольшого, но выкладываемого публично проекта (например, perl-модуля на CPAN) делится на 3 примерно равные части — код, тесты, документация+деплой. Так что да, тесты удваивают время на написание кода, но не общее время проекта (возможно именно с этим фактором связана оценка «раза в 1.5» в предыдущем комментарии Tiendil).

          Но нельзя забывать, что как правило на сопровождение проекта уходит на порядок больше времени, чем на начальную разработку, и вот это время наличие тестов созданных при начальной разработке сильно сокращает! Так что в конечном итоге с тестами работать значительно проще и быстрее.
          • 0
            А вот это, кстати, спасибо. Время на пакетирование/деплой часто в проект не включают, и ещё хуже, не делают. А от этого становится совсем печально.
          • 0
            Есть известное выражение «Typing is not the bottleneck». Основная часть работы это все же анализ требований и построение модели. В тестах это повторно делать не надо.
            • +1
              Как будто тесты не требуют своего собственного уютного мирка с всякими моками да фреймворками, вокруг которых нужно ровно так же думать, читать и планировать.
              • 0
                Это уже архитектура тестов, изначально разговор не про это. Что касается архитектуры тестов, то она достаточно тривиальна и создается обычно в начале проекта, дальше все однотипно. Тесты сложно начать писать — это правда, но потом достаточно просто.
          • +6
            Ваша идея будет работать (со скрипом), если тесты и код пишут разные люди, создавая две разные модели.

            Предложите тест, который, не вычисляя факториала, сможет протестировать функцию «Факториал».
            Предположим, что в голове у разработчика — идиосинкразия, и он не знает, что 0!=1.
            Тогда он и в программе, и для теста накатает один и тот же код, который сам себя проверит и сам себе докажет свою неправильную правильность.

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

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

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

            Помните правило импликации — ложная посылка всегда порождает истинный вывод?
            • 0
              Вы говорите «разработчик». Тесты одному человеку не нужны. Они нужны в проектах на несколько людей, основное, чтобы один мог менять код, не ломая работу другого человека.

              Тесты становятся необходимыми, когда в проекте не остаётся человека, который знает в деталях все подсисемы.
              • +1
                Здесь я подразумеваю, что разработчик и автор тестов — одно лицо, из этого не следует, что это — единственное лицо в разработке.

                По второму пункту — согласен, при условии, что тесты формально доказаны. Так что да, хорошие тесты порождают двойную работу.
                • 0
                  > согласен, при условии, что тесты формально доказаны

                  Не обязательно. Правило 80/20 знаете? Никто и не ставит задачи создать «систему, которую невозможно сломать».
                  • 0
                    Я говорю с точки зрения теории. То что уважаемые практики задвигают теорию взад и интересуются в первую очередь экономической стороной вопроса — это их личное дело.

                    И задачи такие ставят (медицинское ПО, системы управления полетом, ПО для моделирования, управление сложными производствами, криптография, ядра операционных систем, ...), только гораздо реже чем всякие дорвеи, дейтинги, складской учет и прочее.
                    • +3
                      То, что разработчики интересуются экономической стороной вопроса, это не их личное дело, а обьективная необходимось компании в которой они работают.

                      Я представляю что такое формальные методы, одно время увлекался этой темой. Но поймите же что критически важные системы — это капля в море, и теория актуальна для это капли.

                      Вы вот теоретик, а зачем-то решили учить практиков, хотя вот у вас даже понимания нет проблематики, по вашим словам системы это или супер-критичная-крутая-система-которой-только-и-стоит-заниматься, либо какая-то шняка вроде дейтинга. То, что вы называете, это все ничтожные доли. Существует огромное количество сложнейших систем, разработка которые с применением формальных методов является достаточно дорогой, что перекрывает даже любые возможные финансовые потери в связи с ошибками. Любой бизнес имеет риски, и имеет прибыль. Бизнес никогда не существует при нулевых рисках, это является нормой, он лишь оптимизирет эти риски, а не строит формальную модель, исключающую эти риски.
                      • +1
                        В качестве примеров систем я привел крайние варианты, я понимаю, что есть формальный критерий, а есть экономический.

                        Если судить по экономическому критерию, правы безусловно вы. Если судить по критерию «формально, ошибок нет» — правы теоретики.

                        То что социум чаще всего требует работы по экономическому критерию — отдельный вопрос, далеко за рамками этого обсуждения.
                      • 0
                        Для таких задач есть свои методики разработки, как раз основанные на формальных преобразованиях, где код играет совсем не главную роль.
                  • +16
                    >Тесты одному человеку не нужны.
                    Если в таком ракурсе смотреть, то тесты нужны полезны, когда проект перестаёт вмещаться в память разработчика. Не важно 1 он, 10 или 100500. Например я 2 года работаю над проектом в качестве единственного разработчика, тесты очень помогают.
                    • +1
                      Да. Но это разные задачи. В условиях одного разработчика — это оффлоадинг памяти на компьютер (о проекте), а в случае группы разработчиков — метод снижения социальной напряжённости и рисков конфликтов при внесении изменений (работает — не трогай).
                      • 0
                        Про социальную напряжённость не понял. Поясните?
                        • +6
                          У одного разработчика болит в одном месте и он фиксит, это вызввает боль у другого, у которого ЕГО кейс ломается. Я говорю про гигантские проекты с сотнями разработчиков, которые друг друга в глаза не видели и работают на разные компании (openstack — хороший пример).

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

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

                        Скажем, я бы трясся над каждой строчкой при переписывании YaLinqo (LINQ для PHP) под новые фичи языка, если бы у меня не было 100%-ного покрытия.
                    • +2
                      >если тесты и код пишут разные люди, создавая две разные модели.
                      Это не обязательно, модели достаточно отличаются, чтобы их мог писать и один человек.

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

                      Возможности формального доказательства пока нет и в ближайшее время не будет, говорить о нём смысла нет. Нужно использовать то, что есть и работает.
                      • 0
                        Как это возможности формального доказательства нет? Возможности формального автоматического доказательства по голому исходнику — нет. И не будет, так как это невозможно в общем случае (теорема Геделя).
                        И вариантов не бесконечно много, а просто «очень много».

                        А возможность искусного доказательства математическими методами — пожалуйста, сколько угодно. Берем спецификацию на задачу, на язык, на библиотеки — и доказываем. Это теория делать не запрещает.
                        • 0
                          И вариантов не бесконечно много, а просто «очень много».

                          Например любая хеш-функция на вход принимает произвольное количество бит — множество входных параметров у этой функции бесконечно.
                          • 0
                            Любая хэш-функция на достаточно большом наборе данных когда-нибудь зациклится.
                            • 0
                              Ну вот вам и нужно проверить, что при аргументах из бесконечного подмножества области определения функции {0, P, N, K, ..}, значение функции одинаково.

                              Ещё пример: split строки по символу. Вход — строка произволной длинный, выход — массив произольной длинны. Коллизий тут не будет.
                              • 0
                                Значения, с которыми работают математические функции компьютера всегда берутся из счетного и конечного множества.

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

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

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

                                  • 0
                                    Как это аппарат математики нельзя применять к реальному миру?! А физики, описывая реальность математикой, чем по вашему занимаются? Например, GPS в телефоне не врет только потому, что использует выводы ОТО, которая математически позволяет рассчитать поправки на искажение времени вблизи массивного тела — нашей планеты.

                                    Или вы считаете, что математика — это так, «заумь»?

                                    По поводу бесконечных входных данных — для обработки их нужна бесконечная память или бесконечное время. У реального компьютера таковых нет, он всегда работает с конечными и счетными данными.
                                    • 0
                                      >Или вы считаете, что математика — это так, «заумь»?
                                      Я так не считаю, а вот Вы так читаете, видимо.

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

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

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

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

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

                                        Относительно единой теории всего — это вопрос не в плоскости применения математики к описанию реального мира, а в плоскости достаточного финансирования в исследования. Вопрос просто остается открытым.

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

                                        Ваша статья пытается спорить с идеями Дейкстры о хороших компьютерных программах. Вот только критерии «хорошая программа» у вас другие, поэтому спор — бесполезен.

                                        У вас хорошая программа — проданная программа, приносящая прибыль.

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

                                        Работая без доказательства вы систематически совершаете систематическую ошибку выжившего, вот и все.
                                        • 0
                                          >Вы привели аргументы, которые не показывают, что математику нельзя применять к реальному миру.
                                          Я привёл аргументы, показывающие, что математику сложно применять к реальному миру.

                                          >У вас хорошая программа — проданная программа, приносящая прибыль.
                                          Хорошая программа — программа, приносящая пользу. Шире — законченная программа, обеспечивающая решение задачи с необходимым уровнем качества.

                                          Деньги — далеко не первый критерий.

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

                                          • 0
                                            Я привёл аргументы, показывающие, что математику сложно применять к реальному миру.

                                            Я об этом и написал в своем комментарии.

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

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

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

                                              К сожалению, и с формальным доказательством мы не можем это утверждать. Нет способа гарантировать полноту доказанной модели. Она, банально, может не покрывать все случаи (о которых, например, разработчики забыли).
                                              • 0
                                                Сама технология доказательства требует предъявления строгих аргументов по каждому пункту доказательства. Так как компьютерная программа всегда работает с конечным набором данных, этот набор может быть всегда оценен, классифицирован и исследован математической индукцией.

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

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

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

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

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

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

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

                                                      >В том то и положительность формальных методов…
                                                      Вы можете привести практические примеры использования этих методов? Я бы с ними с радостью ознакомился. Потому как критерием полезности, как раз, является практика. Без неё обсуждать «удобство» и «лёгкость» использования крайне сложно.

                                                      • 0
                                                        Самолетом когда-нибудь летали? По для самолетов создается с использованием стандарта DO-178B, в котором есть требование как формального доказательства корректности программы, так и полного покрытия этой программы тестами (что эквивалентно).

                                                        Разработка ПО авионики
                                                        Архитектура систем управления самолётом
                                                        • 0
                                                          Спасибо, отпишусь когда прочитаю.
                                                          • 0
                                                            Прочитал обе статьи, погуглил про стандарт (к сожалению, сам текст стандарта найти не удалось).

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

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

                                                            Построение же высокоуровневых формальных моделей (и их проверка) с моей точки зрения и есть дублирование, т.к. они являются дубликатом того, что реализуется в коде.
                                        • 0
                                          >Например, GPS в телефоне не врет только потому, что использует выводы ОТО, которая математически позволяет рассчитать поправки на искажение времени вблизи массивного тела — нашей планеты.

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

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

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

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

                                            Вы странно излагаете методологический вопрос о применимости теорий. Не «ОТО верно абсолютно», а «ОТО применима только при ограниченных условиях — массы тел такие-то, скорости такие-то, размеры такие-то». И любая математическая модель «выходит в мир» с четко прописанными условиями «данная модель работает только при таких допущениях: — и далее длииииинный список допущений, в который кстати неявно входят и аксиомы арифметики вещественных чисел».

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

                                            Разумеется, все в мире происходит с определенной вероятностью. Вероятность например того, что после того как я возьму с полки утюг, подниму на вытянутой руке, отпущу и он грохнется на пол, испортив паркет, равна 99.999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999 — черт его знает, сколько там девяток.

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

                                            В своих «Избранных статьях» Дейкстра как раз приводит пояснение того, почему обычные инженерные методы испытаний не годятся для дискретных программ.
                                            • +1
                                              >В реальном мире большинство законов обладает определенной локальностью

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

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

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

                                              > И любая математическая модель «выходит в мир» с четко прописанными условиями «данная модель работает только при таких допущениях

                                              Это вы, простите, снова путаете «выходит в мир» и «начинает преподаваться на мехмате». В мир ОТО вышла когда описала поведение перигелия меркурия — одного-единственного ключевого теста. (+ в первом приближении она переходит в ньютоновское тяготение). Физики никогда особо не парились по поводу отсутствия или даже откровенного нарушения математической корректности и обоснованности, если удавалось ухватить за хвост какое-то важное свойство реальности. Я уверен, что в истории науки есть множество случаев, когда математически незавершенные и не вылизанные модели десятилетиями применялись в инженерной практике — куда уж дальше в мир-то выходить?

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

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

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

                                              Вот в программной инженерии то же самое. Есть какие-то совсем базовые модели, доказуемо корректные, а что в них не влезает (т.е. 99.999 программного кода) — проще подогнать по результатам корпуса тестов. Формальная верификация, кмк, имеет очень ограниченную область, где она себя оправдывает — недурно было бы иметь библиотеки шифрования с формально доказанной корректностью. Недурно было бы иметь, скажем, ядро встраиваемой операционки реального времени с доказанной корректность (насколько я знаю, есть парочка таких). Еще пара дюжин примеров общеупотребимых компонент, где на это стоило бы потратить время — может и найдется. Ну и в узких областях типа тех же шаттлов да АЭС. В остальных случаях, я уверен, это не оправдает себя.
                                              • 0
                                                Не очень понимаю, в чем разница с практической точки зрения.

                                                Разница не где-то там в практике, а в методологии: на настоящий момент нет абсолютно истинных физических моделей — есть модели с ограниченной применимостью. Мне даже слезать со стула не надо, чтобы оказаться «в точке пространства, где ОТО дает сбой» — ОТО не работает для квантовой механики совсем.

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

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

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

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

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

                                                Применяя тесты по ограниченному и неполному набору мы намеренно отказываемся от имеющейся у нас информации.

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

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

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

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

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

                                                  > В частности, нам заранее известно, что компьютерная программа работает нелинейно и эта нелинейность — существенна.

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

                                                  Да и вообще: формальное доказательство само по себе — ни что иное как тест. Вы просто скармливаете текст теоремы биологическому компьютеру в своей черепной коробке — и он, пошелестев извилинами, вычисляет значение логической функции на заданных входных данных, и говорит «похоже, истина»/«прохоже, вранье». Степень надежности этого вычисления невысока, поэтому используется множество вычислителей, слегка отличающихся по параметрам, и итоговый результат берется по большинству. То есть «формальное доказательство» — это всего лишь большинство по результатам N экспериментов с вычислением логического выражения на разных ненадежных вычислителях.

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

                                                  Мое мнение — что для 99% программных систем имеет смысл инвестировать в обучение методологии тестирования, в разработку тестовых фреймворков, в грамотное проектирование, в code review и корпусы тестов. Формальные методы здесь могут дать пищу для размышления — например, если я знаю теорию конечных автоматов, я могу спроектировать свой код так, чтобы структура этого автомата была явно видна, и я могу спроектировать корпус тестов так, чтобы он, по возможности, проверял все множество состояний и переходов — и это будет и проще, и даст более надежный результат. (А если я не знаю про конечные автоматы, я, скорее всего, буду проектировать корпус тестов вслепую). Но формально верифицировать этот код скорее всего окажется на порядок дороже — а результат будет тот же. При этом устойчивость формального доказательства к изменениям кода (тому же рефакторингу) очень низка, устойчивость корпуса тестов гораздо выше
                                                  • 0
                                                    С учетом того, что наш мир состоит из тестов и только тестов, достаточно в процессе формальной верификации заменить жесткую логику нечеткой. Тогда и ответы будут в виде «вероятность того — X%, вероятность этого — Y%. Вероятности выданы с доверительным интервалом Z сигм.»

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

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

                                                    О том, что есть разные критерии годности программы я написал (выше и ниже) уже несколько раз, об областях, где мы вынуждены применять столь жесткие меры к контролю качества я также написал.
                                                    • 0
                                                      >С учетом того, что наш мир состоит из тестов и только тестов, достаточно в процессе формальной верификации заменить жесткую логику нечеткой. Тогда и ответы будут в виде «вероятность того — X%, вероятность этого — Y%. Вероятности выданы с доверительным интервалом Z сигм.»

                                                      Ничего принципиально не изменится по сравнению с жесткой логикой — в жесткой логике вам нужны аксиомы (==утверждения, принимаемые со 100% вероятностью), а в нечеткой логике вам нужны нечеткие аксиомы (утверждения, принимаемые с известной вероятностью). Ни то, ни другое в реальности взять неоткуда — из тестов вы не можете извлечь ни точные утверждения, ни точные утверждения об известной вероятности неточных утверждений, ни точные утверждения об известном распределении вероятности неточных утверждений, ни точные утверждения о…

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

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

                                                      Без знания особенностей реализации в общем случае вы не сможете создать такой корпус тестов иначе как полным перебором предметной области — что, как правило, неприемлемо по соображениям производительности. А зная особенности реализации — вам придется менять тесты при изменении реализации.

                                                      >В данном споре я представляю сторону товарища Дейкстры, на которого неоднократно ссылаюсь.

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

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

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

                                                        Без знания особенностей реализации в общем случае вы не сможете создать такой корпус тестов иначе как полным перебором предметной области — что, как правило, неприемлемо по соображениям производительности. А зная особенности реализации — вам придется менять тесты при изменении реализации.


                                                        Это утверждение в частности еще раз показывает несостоятельность идеи, представленной в статье — мы всегда можем так запороть программу или тесты, что они перестанут взаимно верифицировать друг друга.
                                                        • 0
                                                          мы всегда можем так запороть программу или тесты, что они перестанут взаимно верифицировать друг друга.

                                                          Я думаю всему виной неверное представление о цели тестирования. Тест изначально не допускает знание реализации модели, только интерфейса. Таким образом, модель для теста — черный ящик со входом и выходом. И нет другого 100 процентного способа ее проверки, кроме как полный перебор. А если Вы своим тестом залезите в реализацию модели — потеряете основное качество теста — возможность переписывать, рефакторить, оптимизировать реализацию, не трогая тест. Возможность не трогать лишний раз код важна из прагматических соображений соображений, потому как все что Вы трогаете, любое Ваше изменение кода может оказаться ошибкой, человеческий фактор и т.д.
                                      • 0
                                        То, что в памяти конкретного компьютера мы не можем сохранить строку бесконечной длины не означает, что нельзя написать функцию, которая будет работать со строкой любой длины.
                                        • 0
                                          Означает. Если мы хотим поработать с такой строкой, мы должны как-то уметь хранить индекс отдельного символа в строке. Но так как строка бесконечна, индекс — тоже бесконечен — в память он не уместится.

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

                                          Поэтому для проверки корректности таких функций используются математические методы, позволяющие сформулировать критерии полного покрытия такой функции тестами — прогоночными тестами заниматься смысла нет, пространство состояний слишком велико. Но оно конечно и счетно, а значит, может быть испытано методами вроде математической индукции совместно с тестами «по контрольным точкам».
                                          • 0
                                            >Означает. Если мы хотим поработать с такой строкой, мы должны как-то уметь хранить индекс отдельного символа в строке. Но так как строка бесконечна, индекс — тоже бесконечен — в память он не уместится.

                                            Если индекс не уместится в память одной конкретной машины, то вполне может уместиться в память другой.
                                            Я уже запутался, что вы пытаетесь доказать? Если вы говорите об абстрактных математических функциях, то все это верно, если же речь идёт о реальном мире с конкретными компьютерами, то в любом случае, если количество состояний программы достаточно велико, то не имеет значения, конечно оно или нет.
                                            • –1
                                              Не обязательно перебирать все возможные состояния в живом тесте. Достаточно сформулировать критерии того, какие нужно подать на функцию входные значения, чтобы полностью ее протестировать. Относительно тех значений, которые не были поданы на живую, выводы о правильности их обработки делаются путем математической индукции — это и называется «тест с полным покрытием».

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

                                                Давайте на практике, сколько и каких Вам нужно точек чтобы проверить например функцию факториал? И как это спасет, если я псих-программист и не люблю число 125 например:
                                                If (n == 125) throw exception;
                                                
                                                • 0
                                                  Оба ваших комментария во-первых подтверждают несостоятельность идеи тестирования.

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

                                                  Код программиста-нумерофоба в данном случае содержит такое ветвление, и его достаточно очевидно отловить.

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

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

                                                    Идея тестирование — отловить 99 процентов ошибок, большая часть которых человеческий фактор (перепутал имена переменных, знак операции, вызвал код по нулевому указателю), поэтому я и написал о неверном представлении о цели тестирования.
                                                    • 0
                                                      И это не отменяет ревью кода, но взгляд может замылиться и пропустить ошибку.
                                                      И это не отменяет статический анализатор кода, но у него тоже не 100 процентный результат.
                                                      И это не отменяет внедрение автоматических рефакторингов кода и сниппетов, но они тоже ограничены.
                                                      Вот только четвертое не понял, что за узаконенное GOTO?
                                                      • 0
                                                        Про GOTO — ну упомянутый Дейкстра не раз ругался на частое применение этого оператора вместо
                                                        тщательного структурирования и приводил примеры того, как можно любую конструкцию с GOTO обернуть в стандартные структурные блоки.

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

                                                        Идея в том, что хочется иметь комплексный инструмент и методологию для статического, динамического, прогоночного, формального и так далее испытания программ.
                                                        • 0
                                                          Многое из того, о чем Вы пишете уже есть в том же Visual Studio — Resharper: автоматический рефакторинг и сниппеты, статический анализ, нагрузочное тестирование. Что то из этого развито более, что то менее. Но у каждого инструменты своя цель и он никак не заменяет модульное тестирование и другие инструменты. А про GOTO в современных языках давно забыли.
                                                          • 0
                                                            С исключениями — аналогично. Возможность сигануть из блока куда-то в даль далекую способствует запутыванию программы и усложняет ее анализ.

                                                            Исключения — мощный инструмент, позволяющий отреагировать на серьезную нештатную ситуацию, корректно завершить программу или попытаться исправить ситуацию. Но когда бьют из пушки по воробьям — бросают исключения по каждому чиху, это уже проблема правильного использования инструмента.
                                                            • 0
                                                              Использование исключений требует огромного внимания к деталям, в частности, к динамически создаваемым объектам, и особенно к написанию конструкторов и деструкторов.

                                                              Иначе вся мощь этого инструмента преобразуется в лучшем случае в падение по причине необработанного исключения, в худшем — к трудноуловимым утечкам ресурсов.
                                                              • 0
                                                                Использование исключений требует огромного внимания к деталям, в частности, к динамически создаваемым объектам
                                                                Со сборщиком мусора все проблемы с динамической памятью отпадают. Правда появляются другие — проблемы с производительностью. С unmanaged объектами выручает using — end using.
                                                                • 0
                                                                  Язык с управляемым кодом (в виду внесения им в работу программы дополнительной энтропии) является довольно сомнительным кандидатом на место инструмента создания надежных программ.
                                                                  • 0
                                                                    Странно такое слышать. Разработчики языка и среды исполнения, как правило, на порядок превосходят по квалификации среднего прикладного разработчика. При этом они решают за прикладного разработчика те задачи, которые в не-управляемых средах исполнения придется решать ему самому. Проще говоря надежность алгоритма сборки мусора в JVM/CLR на порядок превосходит то, что напишет средний разработчик сам в случае его отсутствия.

                                                                    Эрланг — вполне себе managed runtime — чуть ли не священный грааль надежности, а?
                                                                    • 0
                                                                      Это Ваше теоретическое утверждение сильно расходится с практикой, так как не учитываете энтропию, идущую от программиста (человеческий фактор). Достоинства же управляемого кода — современные методы управления памятью, возможность использовать различные языки, улучшенная безопасность, поддержка управления версиями и четкая организация взаимодействия программных компонентов.
                                                                      • 0
                                                                        … а также пожирание памяти гигабайтами вплоть до ВНЕЗАПНОГО секир-башка-OOM.

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

                                                                        Как только нужно реализовать программу с полным соответствием спецификациям и максимальной защитой от невозможного (по Мерфи) — все эти радости легкого кодирования убираются в сторону и достаются языки без управляемого кода и строжайше бюрократизированные практики. Примеры отраслей я привел выше — ПО для управления оборудованием самолета (не развлекательной системой, а полетом), ПО для медицинской техники и подобное.
                                                                        • 0
                                                                          Дело не в домохозяйках. У каждого инструмента своя область. Когда мы говорим о специализированных микропроцессорах и сильных ограничениях ресурсов — берем ассемблер или С. Когда о тоннах бизнес-логики корпоративного приложения — Вы их тоже попросите на ассемблер перейти? Там любой гений программист утонет.
                                                                          • 0
                                                                            Скажем так, в специализированном компьютере, который входит в состав томографа (относительно нового, 2012 год), особых ограничений ресурсов нет.

                                                                            Тем не менее, там стоит Windows XP (снята с поддержки 08.04 этого года), на которой работает слой совместимости с IRIX (последняя версия вышла в 2006), на котором работает приложение с графическим интерфейсом Motif. Никакого .NET там и близко нет. И Java нет.

                                                                            Когда требуется надежность (доказанная, а не «99%», взятые с потолка), управляемый код — отправляется за борт, потому как сертифицировать программу, на нем написанную, будет почти невозможно.

                                                                            Ассемблер кстати в смысле надежности ничего не добавляет — ПО для Therac-25 было написано на нем, одним «гением», личность которого так кстати и не установили.

                                                                            В очередной раз напоминаю, что сейчас нет средств повышения надежности бизнес-приложений и сайтов-однодневок, кроме шаманских практик с объективно недоказанной эффективностью.
                                                                            Статья Дейкстры вышла в 1985 году, сейчас уже почти 2015. Не монструозного инструмента управления сложностью нет и не предвидится.
                                                                            • 0
                                                                              Тем не менее, там стоит Windows XP (снята с поддержки 08.04 этого года), на которой работает слой совместимости с IRIX (последняя версия вышла в 2006), на котором работает приложение с графическим интерфейсом Motif. Никакого .NET там и близко нет. И Java нет.

                                                                              А слой совместимости IRIX не вносит энтропию? Или может Winows XP идеальна и не содержит ошибок? Или может идеальное железо? Только на оперативной памяти происходит до 4000 ошибок в год.
                                                                              Когда требуется надежность (доказанная, а не «99%», взятые с потолка), управляемый код — отправляется за борт, потому как сертифицировать программу, на нем написанную, будет почти невозможно.

                                                                              Что конкретно здесь мешает сертификации?
                                                                              Ассемблер кстати в смысле надежности ничего не добавляет

                                                                              И я об этом же! Чем более низкоуровневый инструмент, тем больше вероятность ошибки.
                                                                              В очередной раз напоминаю, что сейчас нет средств повышения надежности бизнес-приложений и сайтов-однодневок, кроме шаманских практик с объективно недоказанной эффективностью.

                                                                              Доказательство на практике. Какая бы не была красивая и внутренне непротиворечивая теория у того же Дейкстры — если не прошла этап практики — отправляется на помойку.
                                                                              Не поймите не правильно, я не за сборщик мусора, сайтики, ленивых программистов… Я за разделение труда. Одни пишут ЧТО делать, другие КАК делать. И слоев здесь может быть очень много. Например для графики — КАК выводить изображение пишут в драйверах, зависимых от железа, потом библиотека, независимая от железа, например — DirectX, следующий слой — графический движок и конечный слой, определяющий ЧТО выводить — программа. Так как здесь большая ответственность на нижние слои, вот их и тестируем вдоль и поперек и освобождаем верхние слои от низкоуровневых ошибок, чтобы они занимались своим делом (определяли ЧТО, а не КАК).
                                                                              • 0
                                                                                В вопросе о надежности программ надежность железа берется в качестве аксиомы. Делать надежное железо мы умеем, повышать надежность за счет кратности и сложных методик кодирования (хотя бы ECC) — тоже.

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

                                                                                С Java и .NET работы еще больше, кроме того, в них есть процессы, вроде того же GC, которые могут приступить к работе неожиданно для программиста. Если же GC управлять вручную, удобство куда-то улетучивается.

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

                                                                                «ЧТО делать» в программировании — это декларативный подход, LISP, SQL и их друзья. Это как раз языки, где программист описывает, что он хочет получить, а среда решает, КАК это получить.

                                                                                «КАК делать» — императивный подход, большинство современных ЯВУ.

                                                                                Так что даже когда программист изволит ворочать мегатекселями через DirectX, он все равно пишет «как ворочать», а не «что ворочать».

                                                                                И любимые бизнес-процессы обычно удобнее описывать в терминах «КАК», приправляя иногда запросами к базе, написанными на языке «ЧТО».
                                                                                • 0
                                                                                  В вопросе о надежности программ надежность железа берется в качестве аксиомы.

                                                                                  Ну кроме железа есть еще операционная система и драйвера, надежность которых сходу не оценить. Тоже берем аксиомой?
                                                                                  Чем более высокоуровневым является инструмент, тем сложнее однозначно описать его поведение.
                                                                                  Да наоборот легче, потому как все, что уровнем ниже — протестированная вдоль и поперек аксиома. Пусть она занимает 40 страниц в маленькой книжке, но ее надо протестировать вдоль и поперек один раз и пользоваться ею как аксиомой. А не тестировать каждый раз заново.
                                                                                  С Java и .NET работы еще больше, кроме того, в них есть процессы, вроде того же GC, которые могут приступить к работе неожиданно для программиста
                                                                                  Ну да, в многозадачной ОС ничто не гарантирует непрерывного выполнения, есть еще куча прерываний от устройств и ядра ОС.
                                                                                  • 0
                                                                                    Про практику — математика все время своего существования использует исключительно методологию, описанную Дейкстрой. Он лишь предложил расширить область ее применения.
                                                                                    Я как раз про это его расширение пишу, а не про всю математику. Какие то из его предложений действительно прошли практический этап — нету GOTO например в современных языках. Интересно было бы узнать какие не прижились? Возможно они не были хорошо описаны с точки зрения практики.
                                                                                    • 0
                                                                                      Точка зрения большинства практиков ИТ сейчас такая: «Хватай мешки, вокзал отходит!».

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

                                                                                      • 0
                                                                                        Точка зрения большинства практиков ИТ сейчас такая: «Хватай мешки, вокзал отходит!».
                                                                                        Ну неправда. Шаблоны проектирования (порождающие, структурные, стратегии), принципы проектирования (SOLID), куча разных инструментов (Intelisens, сниппеты, рефакторинг, статический анализ), куча специализированных библиотек, фреймворков. Все это шаманские практики? Да сам Дейкстра много вложил в структурное программирование — некое основание для императивных языков. Но с того времени прошло очень много других изменений.
                                                                                    • 0
                                                                                      Так что даже когда программист изволит ворочать мегатекселями через DirectX, он все равно пишет «как ворочать», а не «что ворочать».
                                                                                      Не не. На верхнем уровне программист или дизайнер загружает модель, выгруженную из 3D Max например и ворочает ее, посылая команды движку. Основной вопрос для него — какую модель взять и ЧТО с ней сделать, то есть вопрос ЧТО. Графический движок анализирует формат вершин и определяет нужные для отрисовки шейдеры и передает команды отрисовки ниже DirectX. DirectX выполняет независимый от железа код, а зависимый отдает драйверам. И чем ниже код, тем больше он отвечает на вопрос КАК сделать, независимо от языка на котором написан.
                                                                                      И любимые бизнес-процессы обычно удобнее описывать в терминах «КАК»

                                                                                      Декларативный подход часто более удобный. Тот же LINQ например значительно уменьшает размер программы и увеличивает ее читаемость в большинстве случаев.
                                                                                      • 0
                                                                                        Здесь можно также сказать, что бизнес-требования как правило изложены декларативным языком. Отсюда и вытекают интересности: компьютер, по его структуре, предназначен для написания императивных программ, а требования изложены декларативно.

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

                                        >Предположим, что в голове у разработчика — идиосинкразия, и он не знает, что 0!=1.
                                        Отсутствие тестов также не поможет в этой ситуации.

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

                                          Пост очень близок к практической разработке.

                                          … которая, в свою очередь, иногда очень близка к «фигак — в продакшен». Что в общем-то ясно: у практической разработки нет цели сделать идеально.
                                          • +2
                                            Отрицания полезности стороннего ревью в посте тоже вроде не было. Автор данного метода повышения качества вообще не касался. Если ошибаюсь — поправьте.
                                            Если писать ПО для космического корабля или мед. оборудования — согласен, тут и тесты не тесты, а целая наука и стороннее ревью не для галочки. Но когда речь идет о ПО для домохозяйки с интерфейсом «сделать хорошо», то «фигак — в продакшен» — обычая практика, и тестов там будет волне достаточно.

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

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

                                              Я не отрицаю саму идею тестов, я отрицаю тесты без формального сопровождения корректности и утверждение, что программа — тест для тестов.
                                              • +1
                                                Ваша позиция ясна и хороша. Но все же находится ближе к теории, чем практике.
                                                Нередко в проектах толком не формализована сама задача, а о формальном сопровождении корректности тестов можно только мечтать. И это печально.
                                                • 0
                                                  Благодарю за понимание!
                                        • 0
                                          Если тест испытывает все возможные варианты ветвления тогда программа вобщем-то и не нужна — достаточно в процессе тестирования сохранить все входные данные и сопоставить им все выходные выданные программой.
                                          • 0
                                            Проверить, что тест заставит алгоритм пройти по всем сочетаниям ветвлений не эквивалентно подаче на алгоритм всех возможных вариантов входных данных, подумайте над этим.
                                            • 0
                                              Да, согласен — погорячился.
                                            • 0
                                              Во-первых, это невозможно при наличии хоть немного нетривиальных циклов. Выход на первой итерации, на второй и на миллиардной — это разный control flow, ошибка может возникать только на некоторых итерациях.

                                              Во-вторых, в истории программирования известно множество ошибок, которые содержались в коде без ветвлений. Переполнение при бинарном поиске, например.
                                              • –1
                                                Это не «формально невозможно» а «практически очень сложно» — две большие разницы

                                                В приличном коде перед любой арифметикой стоит ASSERT, который проверяет, что при данных входных не будет переполнения, деления на 0, вычисления четного корня из отрицательного числа и других глупостей. А ASSERT — ветвление.
                                                • 0
                                                  Это в том случае, если вы в состоянии подумать обо всех граничных случаях. Не надо переоценивать свой разум: ошибка в алгоритме binarySearch в самых стандартных библиотеках была не замечена десятилетиями. Многие ли люди ставят правильный assert перед каждым вызовом Math.abs? Вы лично ставите?

                                                  Именно что формально невозможно: итераций может быть сколь угодно много. Для любого количества итераций, которое вы проверили, возможно такое количество, которое вы не проверили. Если внутри итерации есть ветвление, то проблемы с проверкой возникнут гораздо быстрее: на каждой итерации вы можете пройти либо по первой, либо по второй ветке. Для 20 итераций у вас уже более миллиона вариантов выполнения. Добавили одну итерацию и написали вдвое больше тестов?
                                                  • 0
                                                    Компьютер является конечным автоматом. Это значит, что чисто формально любую программу можно проверить полным прогоном. Да, это практически бессмысленно.

                                                    Поэтому проще проверять покрытием по контрольным точкам.

                                                    Для цикла кстати не обязательно проверять на живую все итерации. Доказательство корректности для цикла строится из двух частей:
                                                    1. Доказать, что при таких входных параметрах цикл неизбежно завершится
                                                    2. Далее, тело цикла рассматривается и доказывается как отдельная программа
                                                    • 0
                                                      Как вы собираетесь в общем случае доказать, что цикл при данных параметрах неизбежно завершится? И про assert перед каждым вычислением абсолютного значения целого числа ответьте пожалуйста. Можете показать свой код, где вычисляется абсолютное значение.
                                                      • 0
                                                        Про проблему остановки:
                                                        В любой прикладной программе все циклы должны когда-то завершится либо выдачей решения либо сообщением об ошибке «превышено максимальное число итераций».

                                                        Я знаю о риске переполнения у границ разрядкой сетки целых чисел.

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

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

                                                        ASSERT строится не на тупой проверке, а на формальном доказательстве, которое выполняется математически.
                                                        • 0
                                                          К сожалению, по вашим общим словам так и не становится понятно, как правильно писать тесты и разрабатывать программы и почему же в реальном софте столько багов.
                                                          • 0
                                                            Почитайте, очень познавательно. Именно этот человек является автором мема Considered harmful в отношении оператора GOTO, и именно он выступал против тестов программ, аргументируя это необходимостью предъявить тесты тестов тестов.

                                                            А багов столько потому, что экономически выгодней разработать и продать что есть, а не выискивать жуков повсюду убойным математическим аппаратом.
                                                          • 0
                                                            >> Так вот, я буду следовать этому правилу и банально не допущу того, что у меня числа в программе доберутся до границ разрядной сетки.
                                                            Хорошее намерение… до тех пор, пока заказчик зачем-то не хочет работать с числами, которые находятся на границе порядка (т.е., максимально допустимая разрядность/точность, существующая в платформе). Следование вашему правилу обозначает увеличение сложности разработки (потому что придется переходить в области, не поддерживаемые платформой из коробки). Я уже не говорю о таких мелочах как объемы данных и скорость их обработки.
                                                            • 0
                                                              Начнем с того, что математические алгоритмы с над вещественными числами реализуются так, чтобы решаемая ими задача была обезразмерена и норморована — то есть максимальное число в задаче по модулю будет не более единицы.

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

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

                                                              Верхолаз берет с собой на гору веревку, которая имеет многократный запас прочности на разрыв, вы же предлагаете ему взять более дешевую веревку, которая выдерживает ровно вес верхолаза. После этого, верхолаз будет убит лишним пончиком или случайным порывом ветра, который его раскачает.
                                                              • 0
                                                                >> Если же работать в целых числах без запаса разрядной сетки, кто-нибудь получит зарплату в минус 32767 у. е.
                                                                Или программа выдаст ошибку — что, очевидно, предпочтительнее.

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

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

                                                                  Если мы хотим скорости, мы будем писать на чем-то вроде C:

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

                                                                  Если же используется песочница, то есть интерпретируемый язык, или язык с JIT, о каком выжимании ресурсов платформы может идти речь?

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

                                                                  Я предпочитаю треугольник качество-требования-ресурсы. Увы, я зажрался.
                                                                  • 0
                                                                    >> Это надо перед каждой операцией пичкать проверки
                                                                    Да, надо. Это плата за безопасность.

                                                                    >> которые будут кушать ресурсы, о которых так печется заказчик.
                                                                    А кто вам сказал, что заказчик печется о ресурсах?

                                                                    >> Если же используется песочница, то есть интерпретируемый язык, или язык с JIT, о каком выжимании ресурсов платформы может идти речь?
                                                                    А никто и не говорил о «выжимании ресурсов платформы».

                                                                    >> С точки зрения заказчика «программа посчитала фигню» и «программа при расчете выдала ошибку» — вещи эквивалентные
                                                                    Отнюдь. Когда программа выдала ошибку, пользователь точно знает, что результатом работы программы пользоваться нельзя. А вот когда она посчитала фигню, пользователь не знает, что она посчитала фигню, и отправит результат дальше по цепочке.

                                                                    >> Я предпочитаю треугольник качество-требования-ресурсы.
                                                                    Это тот же самый треугольник, так что говорить о предпочтениях достаточно странно.
                                                                    • –1
                                                                      А кто вам сказал, что заказчик печется о ресурсах?

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


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

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


                                                                      Дыра в логике. Из того, что программа не выдала ошибок, а выдала результат еще не следует, что результат верный. Это будет следовать только из отдельного формального доказательства того, что программа безупречна. Без этого программе можно только верить… ну скажем на основании того что она «всегда верно считает» или «вчера работала верно». В большинстве прикладных случаев этого достаточно конечно же.

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

                                                                      Вы таки заметили, что на первое место я поставил качество?

                                                                      Кстати, а как вы собираетесь проверять, что суммирование a+b не вызовет переполнения, не привлекая дополнительных разрядов?
                                                                      • 0
                                                                        >>Это утверждение эквивалентно требованию «полностью использовать ресурсы вычислительной платформы на решение задачи, не оставляя никаких запасов на надежность».

                                                                        Нет. Заказчику плевать на ресурсы вычислительной платформы, он просто хочет, чтобы площадь участка описывалась числом (38,19) (38 знаков суммарно, 19 — справа от запятой).

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

                                                                        >> Вы таки заметили, что на первое место я поставил качество?
                                                                        А это не важно. Когда говорят о треугольнике, имеется в виду, что соотношение определяется позицией внутри треугольника, так что порядок именования вершин никого не волнует.

                                                                        >> Кстати, а как вы собираетесь проверять, что суммирование a+b не вызовет переполнения, не привлекая дополнительных разрядов?
                                                                        Использовать платформу, которая делает это за меня.
                                                                        • 0
                                                                          Так платформа, которая что-то делает «за вас» будет это делать, привлекая дополнительные разряды. То есть мы показали, что без привлечения дополнительных разрядов этот контроль сделать просто невозможно.

                                                                          Если заказчик изволит просить 19 знаков после запятой, вычисления необходимо выполнять на платформе, у которой 25 знаков после запятой. Так о чем наш спор-то?
                                                                          • 0
                                                                            >> Так платформа, которая что-то делает «за вас» будет это делать, привлекая дополнительные разряды.
                                                                            А вот это происходит прозрачно для меня.

                                                                            >> Если заказчик изволит просить 19 знаков после запятой, вычисления необходимо выполнять на платформе, у которой 25 знаков после запятой.
                                                                            Нет. В зависимости от задачи, вычисления необходимо либо выполнять с точностью 25 знаков после запятой, либо на платформе, которая позволяет выполнять вычисления с 19 знаков после запятой без скрытых ошибок.
                                                                            • 0
                                                                              Реализовать эти вычисления можно только привлекая дополнительные разряды, увеличивая требования к памяти и снижая скорость обработки данных — то есть реализуя все те плохие вещи, с которых наш с вами спор начался. Без этого — никак.
                                                                              • 0
                                                                                Все зависит от того, кто и какими средствами это выполняет. Я не вижу смысла увеличивать точность прикладных вычислений, если платформа позволяет выполнять их с нужной заказчику точностью без скрытых ошибок. Для меня, как разработчика, это не содержит дополнительных накладных расходов.
                                                                                • 0
                                                                                  То есть если вы не знаете о существовании дополнительных накладных расходов, их как бы и нет.

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

                                                                                  Ваше «19 знаков без скрытых ошибок» фактически означает «25 знаков со всеми погрешностями» и реализуется именно таким образом.
                                                                                  • 0
                                                                                    >> то есть если вы не знаете о существовании дополнительных накладных расходов, их как бы и нет.
                                                                                    Не так. Если платформа мне говорит, что для обработки такого числа нужно n байт, то я n байт и считаю.

                                                                                    И самое главное — для меня, как для разработчика, нет головной боли с тем, чтобы увеличивать эту точность вручную, а потом заниматься обратными приведениями.
                                                                                    • 0
                                                                                      Так платформа и будет хранить в этих байтах значения не на 19 разрядов, а на все 25, спрятав от вас всю умную математику. Вы попросите у нее 30 разрядов, а хранить она будет фактически 36 и считать будет 36. И накладные расходы будут на 36 при точных 30. Только и всего.
                                                                                      • 0
                                                                                        Вот только _мне_ не нужно следовать заявленному вами правилу «твоя разрядная сетка должна быть на 4-6 десятичных знака шире, чем все числа, встречающиеся в задаче». О чем и шла речь с самого начала.
                                                                                        • 0
                                                                                          Это если вместо платформы у вас песочница, которая думает за вас.

                                                                                          Если вы используете C, ваша точность — машинный эпсилон для double — примерно 10^-16. Значит все расчеты будут верны примерно до 10 знака после запятой максимум. Если заказчик попросит больше, придется привлекать тяжелую артиллерию вроде GMP и иметь пенальти по скорости и памяти.
                                                                                          • 0
                                                                                            Не «вместо платформы», а платформа. Знаете, как-то громко называть MS SQL песочницей, м?
                                                                                            • 0
                                                                                              Под «песочницей» следует понимать программное окружение, вычисления на котором выполняются абстрактно от аппаратной платформы. В данном конкретном случае, MS SQL — самая настоящая песочница.
                                                                                              • 0
                                                                                                А, если под платформой понимать аппаратную платформу, то да, конечно. Но аппаратными платформами жизнь разработчика, к счастью, не ограничивается.
                                              • 0
                                                Предлагается вместо формального доказательства корректности каждого шага в программе, сделать тест, который что-то там проверит.

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

                                                З.Ы. Советую почитать классическую книгу Майерса «Искусство тестирования программ», там проблема тестирования и доказательства корректности хорошо описана.
                                                • +1
                                                  Т.е. тестирование в принципе можно рассматривать как «альтернативу» отладке.
                                                  Как с алгоритмами: либо тратишь память (сохраняешь уже вычисленное) — меньше вычисляешь, не тратишь — приходится пересчитывать каждый раз заново.
                                                  Так и здесь: пишешь тесты — меньше, проще и сразу понятно где отлаживать, не пишешь — тяжело локализовать место ошибки, тратишь кучу времени на исправление.
                                                  А как бонус идет то, что тесты можно использовать и через месяц и через год, а отлаживать придется каждый раз заново с нуля.
                                                  Естественно тут тоже не без проблем: тесты как и основной код нужно поддерживать в актуальном состоянии, что требует дополнительного времени.
                                                  • 0
                                                    Тест должен рассматриваться как закрепление уже пройденного материала, но не как контрольная работа.

                                                    Контроль корректности программы возлагается на ревью кода, формальное доказательство и на тесты с формально показанным полным покрытием.

                                                    Утверждение «Я доказал — ошибок нет, вот доказательство» сильнее чем «я протестировал вот этими тестами, и оно не упало», потому как сразу последует вопрос «Докажите, что ваши тесты покрывают все».

                                                    Тест с полным покрытием формально эквивалентен приведению полного доказательства к программе.
                                                    • +1
                                                      Я наверное слишком сильно расписался выше.
                                                      Идея тестирования вообще не в том чтоб доказать корректность.
                                                      Идея как раз наоборот найти ошибки.
                                                      Тестирование это вообще не про корректность.
                                                      Вот что я имел в виду.
                                                      • 0
                                                        Тесты не ловят плавающие ошибки. Никак. Выловить тестом Race Condition или Data Race, которая вылезает с вероятностью 1/100000 — это практически невозможно. Тут только формальное доказательство с привлечением спецификаций на язык, компилятор и архитектуру может помочь.
                                                        • +1
                                                          А я и не говорю, что тесты панацея.
                                                          Но они позволяют сократить время на локализацию проблемы.
                                                          А что отладка, что тестирование параллельных процессов это не тривиальная задача.
                                                          Просто когда есть уверенность в том что простые варианты проверяются тестами можно сосредоточиться на сложных.
                                                          Если ошибка получается из-за банальной опечатки при правки кода, то тесты это быстро отловят, а если проблема с тонкостями многопоточности то тут только человек
                                                          • 0
                                                            Главное, чтобы тесты не создавали ложной уверенности: прошел тесты -> ошибок нет.

                                                            Из посылки «прошел тесты» следует только «тесты ошибки не нашли» и ничего более.
                                                            • +2
                                                              Полностью согласен.
                                                              Тесты это помощник в поиске ошибок.
                                                              Плюс позволяют обнаружить появление ошибки в уже проверенной части при внесении изменений (естественно если на ошибки такого рода уже есть тесты)
                                                              • 0
                                                                Спасибо за понимание!
                                                          • 0
                                                            Ваша позиция может быть более менее обоснованной только если процесс доказательства может быть завершен полностью за конечное число шагов — тогда на выходе получается 100% надежности при конечных затратах, что, конечно, очень козырно.

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

                                                            И это значит, что — со всеми теми сложностями и затратами, что несет формальное доказательство — вы получите на выходе все равно ненулевую вероятность наличия багов. И поэтому ценность формального доказательства не так высока, как вам кажется — фактически, ее нужно оценивать в каждом конкретном случае, с позиции баланса затрат/пользы. Вполне возможно, и даже очень вероятно, что хороший корпус тестов + внимательное ревью может обеспечить приемлемую надежность, при несопоставимо меньших затратах в доминирующем большинстве реальных проектов
                                                            • 0
                                                              Первая аксиома при доказательстве корректности программы:
                                                              1. Вычислитель работает корректно.

                                                              Как следствие, результатом всей этой работы будет вывод:

                                                              Если вычислитель работает корректно, программа корректна.

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

                                                              «хороший корпус тестов» — что это такое? Это такая штука, для которой показано, что прошедшая эти тесты программа даже в случае скрытых ошибок не приведет к катастрофе с нужной вероятностью. А доказать такое счастье можно только формально рассуждая.
                                                              • 0
                                                                >Потом идем к инженеру — разработчику системы, и он дает справку, что его считалка работает с вероятностью 1 ошибка в 1000 лет (утрирую) — это и будет итоговая вероятностная оценка качества работы нашей программы.

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

                                                                >«хороший корпус тестов» — что это такое? Это такая штука, для которой показано, что прошедшая эти тесты программа даже в случае скрытых ошибок не приведет к катастрофе с нужной вероятностью. А доказать такое счастье можно только формально рассуждая

                                                                Каковое доказательство, опять же, в своей основе будет опираться на надежность вычислителя программы, и вычислителя теоремы о корректности. То есть, в конечном счете, на результаты тестов. Другими словами, формальные методы это всего лишь еще одна точка зрения на код программы — со своими плюсами и минусами. Их можно применять фанатично, можно частично, можно вообще не применять — для каждого подхода есть свои области применимости.
                                                        • 0
                                                          Да с чего вы взяли, что мы занимаемся проверкой корректности программ. Вы понимаете на сколько доказательство корректности дороже тестирования? Формальные методы для обычных копраративных систем и сайтов — это адовейший оверинжениринг.
                                                          • 0
                                                            Это зависит от масштаба, особенно в части сайтов. Потому как проверка корректности — защита от дыр в программе (сайт кстати тоже программа). Пока программа является неуловимым Джо — на корректность можно наплевать. Как только аудитория растет… ну можно перефразировать американские «права при аресте»:

                                                            Любая дыра будет найдена и может быть использована против вас

                                                            • 0
                                                              Аудитом безопасности занимаются сторонние специализированные конторы. Изучать и применять формальные методы компании самой обычно не актуально, так как это отдается на аутсорс. Конечно у контор уровня Google есть и свои спецы по верификации, но вы понимаете, что то, что вы говорите про формальные методы актуально для каких-то долей процента разработчиков?
                                                              • 0
                                                                Я это прекрасно понимаю. В рамках этого топика я пытаюсь показать формальную несостоятельность тестов для проверки корректности программы и донести, что тесты без формально полного покрытия ничего не могут сказать об отсутствии ошибок в программе.

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

                                                                  >Понимаете, опираться на низкую вероятность — это большой риск.

                                                                  Я там выше уже отписал, это ваше утверждение не имеет никакой связи с реальность. Риск — это не только вероятность чего-то произойти, это еще и убыток. Вот это сочетания вероятности чего-то плохого и убытка в результате и называют риском. В случае АЭС возможные убытки слишком большие, поэтому там формальные методы оправданы. Если cost-of-failure не настолько большой, все это идет лесом.
                                                      • 0
                                                        Справедливо для небольших проектов, код которых вы знаете. Во времена написания книги, программы, возможно, были проще.

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

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

                                                        Фаззинг важен. Несомненно. Писать проверяющие корректность тесты, трассируя код лишь в уме, стало привычнее, чем постоянно фаззить и погружаться в отладку.
                                                        • 0
                                                          В крупных проектах цель автоматических тестов именно в проверке корректности. Чтобы коллега, сливая ветки, и задевая код, написанный не им, получал некую увереннсть — код в тестируемых ситуациях остался рабочим.

                                                          Не совсем согласен. Уверенность получается за счёт того, что есть некоторый набор критериев, позволяющий проверить что остальная часть системы осталась незатронутой и по прежнему работает так же как и раньше с точки зрения имеющихся тестов.
                                                          Мы не корректность проверяем, а проверяем не внесена ли ошибка в уже проверенный код.
                                                          • 0
                                                            Если проводить аналогию с современным состониянием процесса тестирования, то книга Майерса близка к фаззингу и отладке:
                                                            Напишите тест, который приведёт к нестандартному состоянию.
                                                            Начинайте отладку программы (не тест начинает отладку, а инженер).
                                                            Выясняйте в чем ошибка, исправляете (не тест ищет ошибку, а инженер).

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

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

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

                                                              Пусть пишем и тестируем прошивку для боеголовки. Аспекты:
                                                              • программа пишется в машинных кодах или на сложном языке, который программист видит впервые;
                                                              • программа выполняет относительно простую функцию (при поступлении сигнала А должно выполниться действие Б, и всё);
                                                              • нештатные ситуации и входные данные крайне сложно формировать вручную пользователю;
                                                              • нештатных ситуаций гораздо больше, чем штатных.


                                                              Другой пример. Используя фреймворки и лучшие практики, строится приложение для бухгалтеркого учёта. Проверкой корректности уже эффективнее заниматься сотням автоматических тестов. А нештатными ситуациями лучше заниматься людям. Тут иные аспекты.
                                                              • +1
                                                                Я не говорю, что тесты ничего не проверяют.
                                                                Я целиком за тестирование.
                                                                Просто корректность (с математической точки зрения) и корректность с пользовательской (соответсвие ожиданиям) это на мой взгляд разные вещи.
                                                                Автоматизированные функциональные тесты отлично подходят для тестирования пользовательских сценариев.
                                                                Модульными и интеграционным тестами можно покрыть класс или библиотеку так, что на любых практических данных все будет работать безошибочно.
                                                                Но к корректности (алгоритмической если хотите) это будет иметь не слишком много отношения.
                                                                А что касается практики, то только тесты могут давать некоторую уверенность, что основные, наиболее часто используемые моменты небыли упущены программистом.
                                                                Я совсем не за то чтобы формально доказывать корректность любой программы. Совсем наоборот. Просто нужно понимать, что если ты покрыл программу тестами это вовсе не означает, что в ней нет ошибок.
                                                                • +1
                                                                  Естественно, применяя правильные подходы, можно добиться того, что с тестами вероятность наличия ошибки в коде будет близка к нулю.
                                                                  И на практике этого бывает более чем достаточно.
                                                                  Но тесты в отрыве от других методов, сами по себе, не дают оснований говорить что в коде не содержится ошибки. Это нужно принять и использовать их в повседневной практике.
                                                                  Просто иногда тесты дают ложную уверенность в правильности кода.

                                                                  Протестированная программа != правильная программа.
                                                                  Вот и все. Это нужно понимать и помнить. И тестировать свой код. :)
                                                        • +1
                                                          То, что в голове разработчика неправильная модель, большого значения не имеет. Разработчик существует не в каком-то там ваккууме. Как правило, есть коллектив, есть живые тестеры. Как минимум, в очевидные ошибки они разработчика могут ткнуть. То, что юнит-тесты являются отражением модели задачи в голове разработчика и, в какой-то степени, реальной модели, позволяет выявлять ошибки типа регрессий. Т.е. когда что-то где-то поменяли, а в совершенно противоположном месте кода какой-то функционал перестал работать. Т.е. юнит-тесты позволяют поддерживать код в стабильном состоянии. Они позволяют разработчику работать над новым функционалом не опасаясь за старый. Вроде бы вещи очевидные.
                                                          • +1
                                                            Что касается двойной ошибки — и в тесте и в коде, то вероятность такого минимальна, если бы вы писали тесты, вы бы знали, что на практике такое крайне редко бывает. Ну да, бывает, но из этого следует лишь то, что метод не работает в 100%, но если он работает в 90%, то он эффективен. Тут не формально что-то доказывать нужно, а оценивать экономическую эффективность.
                                                          • 0
                                                            Если тесты содержат какую-то свою библиотеку для работы (например, для доступа к API) — ее, наверное, все же имеет смысл тестировать?