No Bugs, No Flaws или о надежности систем как таковых

    Сегодня просматривая публикацию Егора Бугаенко When Do You Stop Testing!, с удивлением обнаружил, что немногие понимают и задумываются о том, что проблема тестирования и утверждения того, что система не имеет недостатков принципиально не решаема. Это кстати еще актуально и в связи с внедрением электронных выборов, и требованиями со стороны официальных лиц и журналистов доказательств отсутствия дыр в системе безопасности. Например у нас (Эстония) эта дискуссия идет полным ходом, и политики хотят получить стопроцентные доказательства надежности системы электронных выборов. Публичные политики, как правило незнакомы с логикой в её формальном виде. А Юм и Поппер, в лучшем случае, напоминают о каких то скучных философских семинарах, о которых лучше забыть. Но когда я слышу о том, что тестер или сеньор начинает вполне серьезно доказывать, что код протестирован и ошибок нет совсем, мое лицо приобретает это выражение:

    image

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

    Первый момент — логический


    Проблема индукции, которую серьезно рассмотрел Юм, ставит под сомнение саму возможность обоснования целого ряда проблем и вопросов. Например, выведение неких общих выводов из наличия неких частных наблюдений невозможно. Неограниченное количество наблюдений чего либо, не подтверждает истинность утверждения. Карл Поппер, один из невероятнейших гениев в истории человечества, обратил внимание на проблему фальсификации, и стал автором новой парадигмы в философии науки. Какова суть проблемы фальсификации и как это касается нас? Самый известный пример, — это «Черный Лебедь». Черный Лебедь был символом невозможности чего либо в 16 веке в Лондоне. Старый Мир предполагал, что все лебеди белые, поскольку все исторические записи о лебедях описывали их белые перья. И в этом контексте черные лебеди были невозможны, или не существовали. Тем не менее, в 17 веке представитель Старого Мира встретил невозможность в Австралии.

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

    Например, если последние 4,5 миллиарда лет Солнце регулярно (хорошо — хорошо, с неким замедлением) всходило над горизонтом, то это не говорит нам, что Солнце всегда встает над горизонтом. Или любитель парадоксов Б. Рассел приводит пример с индейкой, которую кормят, за которой ухаживают, и она думает, что так будет всегда, пока не настает тот самый день, день Благодарения.

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

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

    Второй момент — вычислительный


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

    Третий момент — инженерный


    Существуют такие ситуации, что мы можем даже знать, что у нас существует некий специфический баг, который рушит нашу систему, потому, что мы наблюдали это в какой либо момент. Мы знаем, что баг есть. Но мы не можем его репродуцировать. Я имею в виду проблемы в мультипоточных приложениях, где правит бал недетерминизм. Нет особых проблем выловить баг, если сервер рушится каждые десять минут. Но что если нам необходимо, чтобы сервер работал несколько месяцев прежде чем проблема снова вернулась. Это в прямом смысле невозможно отладить. Хуже того, как упоминал Paul Butcher, вполне вероятно писать программы, которые содержат мультипоточные баги, которые никогда не проявятся несмотря на то, как тщательно или как долго мы бы тестировали их. Только потому, что обращения потоков к памяти могут быть переупорядочены, не означает, что так и будет сделано. И мы вполне можем быть абсолютнo в неведении о наличии проблем, пока мы не сделаем апгрейд JVM или перейдем на другое железо, где мы внезапно столкнемся с таинственными проблемами, которые никто не понимает.

    Все эти три момента делают само утверждение о том, что багов нет, или о доказательстве безопасности чего либо бессмысленным. Очень большой процент ИТ профессионалов также не понимает этого. Прекрасный пример в посте Егора Бугаенко.

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

    Similar posts

    AdBlock has stolen the banner, but banners are not teeth — they will be back

    More
    Ads

    Comments 15

        0

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


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

          0
          Не спорю, потому что слабо разбираюсь в теме. Но мне показалось странным, что этого нет в посте.
          0
          Да это еще один импенданс между формализмом и реальным миром.
          Плюс формальная верификация имеет отношение к теореме о неполноте Гёделя. Всегда будут существовать предложения которые в рамках данной формальной системы недоказуемы, или же эта система противоречива и/или неполна. По большому счету, Гёделевская неполнота, Тьюрингова остановка, оптимальность по Колмогорову это грани одной и той же проблемы. Что бы мы ни делали, решали бы проблему перебором и различными синтаксическими комбинациями формальных правил, или использовали эвристику в рамках тех же правил, нет возможности принципиально обосновать и доказать все утверждения системы.
          Грубо говоря даже на арифметике мы проваливаемся в «деление на ноль»(метафора). Формальная верификация применима к очень узкому ряду проблем.
            +1

            кстати, https://gist.github.com/edwinb/0047a2aff46a0f49c881 к вопросу о делении на ноль

              0
              Кстати к делению на ноль.

              Сложение, умножение и вычитание можно получить в арифметике Пеано с помощью примитивных рекурсивных функций. И эти операции будут всегда останавливаться. Их всего три операции. Константа(0), Функция Следования(инкремент +1) и собственно Функция Проекции (Рекурсия) которая все связывает. Три действия арифметики реализуются этими концептами. Их достаточно для реализации одного шага машины Тьюринга. Содержимое машины Тьюринга может быть представлено в виде очень большого числа и примитивные рекурсивные функции могут использоваться для чтения/записи или передвижения влево/вправо, но для полноценной работы машины Тьюринга необходимо больше. Поскольку они могут не останавливаться никогда. Также и с делением в арифметике. Когда появляется деление, то для этой операции необходима Функция Минимизации, которая уже не останавливается гарантировано. В случае же нуля, остановки не происходит, почему я и говорил, что деление на ноль и проблема остановки/тестирования это одна проблема по большому счету в Computer Science

              Partial Recursive Functions

              Отличная книга по этой теме.

              Understanding Computation

              Отрывок оттуда.

          0
          Формальная верификация это и есть вычислительный аспект. Теорема Райса применима к ней.
            0

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

              0
              Да есть. Я сам когда то участвовал в разработке таких ассесмент систем для Continious Delivery pipeline.

              Не помню деталей, но для проверки софта AirBus 330 (нового на тот момент) была внедрена такая система, и действительна она снизила риски и нашла много всего невкусного. Но тем не менее это были не все баги, и потом компания сталкивалась с ними в дальнейшем. Но теме не менее по результатам она себя больше чем оправдала. Извините не помню деталей в числах, поскольку давно с этой сталкивался. Вот отрывок из статьи тех времен.
              https://books.google.ee/books?id=OZhCTkrCyRwC&pg=PA153&lpg=PA153&dq=AirBus+a330+software+test+history&source=bl&ots=quLKmzcdgl&sig=SosTfKgQ4GveVSjXGbxIQBIcRu8&hl=ru&sa=X&ved=0ahUKEwi-xrCtjKTTAhVEkiwKHcYqAOkQ6AEIXTAH#v=onepage&q=AirBus%20a330%20software%20test%20history&f=false
              +2
              Да, проблема нерешаема в общем виде. Но всегда ли нужен общий вид?
              Дано: реализовать утилиту /bin/true.
              Решение:
              int main(void) { return 0; }
              Найдите ошибку.
                0
                Не всегда нужен общий вид. Но даже в вашем выраженном примере в действительности выполняется не этот код. Он транслируется на все более низкие уровни абстракции, где последним уровнем являются по видимому электроны, которые подчиняются законам физики и выполняют computation. Но между вашим кодом и электронами множество слоев, в том числе и операционная система, и внутреннее устройство чипа и т.д. и т.п. Это все должно приниматься во внимание.
                  0
                  Это все должно приниматься во внимание.

                  А оно и принимается — компиляторами, микрокодом железа, ядром ОС и библиотеками, предоставляющими интерфейс к ОС.

                0
                Бугаенко, не Бугаева)
                  0
                  Pardon ) Пальцы жили своей жизнью в момент печатания.
                  0
                  Для понимания тестирования довольно-таки полезная статья. Автор молодец!

                  Only users with full accounts can post comments. Log in, please.