Comments 15
Проблема формальных доказательств в том, что нам нужно формальное описание. А еще нам нужно верифицировать формальное описание, чтобы оно соответствовало реальном миру и нашим желаниям, т.е. нам нужно формальное описание формального описания. Вытекающая из этого проблема очевидна.
В итоге формально верифицировать можно, в лучшем случае, лишь малую часть программы.
Да это еще один импенданс между формализмом и реальным миром.
Плюс формальная верификация имеет отношение к теореме о неполноте Гёделя. Всегда будут существовать предложения которые в рамках данной формальной системы недоказуемы, или же эта система противоречива и/или неполна. По большому счету, Гёделевская неполнота, Тьюрингова остановка, оптимальность по Колмогорову это грани одной и той же проблемы. Что бы мы ни делали, решали бы проблему перебором и различными синтаксическими комбинациями формальных правил, или использовали эвристику в рамках тех же правил, нет возможности принципиально обосновать и доказать все утверждения системы.
Грубо говоря даже на арифметике мы проваливаемся в «деление на ноль»(метафора). Формальная верификация применима к очень узкому ряду проблем.
Плюс формальная верификация имеет отношение к теореме о неполноте Гёделя. Всегда будут существовать предложения которые в рамках данной формальной системы недоказуемы, или же эта система противоречива и/или неполна. По большому счету, Гёделевская неполнота, Тьюрингова остановка, оптимальность по Колмогорову это грани одной и той же проблемы. Что бы мы ни делали, решали бы проблему перебором и различными синтаксическими комбинациями формальных правил, или использовали эвристику в рамках тех же правил, нет возможности принципиально обосновать и доказать все утверждения системы.
Грубо говоря даже на арифметике мы проваливаемся в «деление на ноль»(метафора). Формальная верификация применима к очень узкому ряду проблем.
UFO just landed and posted this here
Кстати к делению на ноль.
Сложение, умножение и вычитание можно получить в арифметике Пеано с помощью примитивных рекурсивных функций. И эти операции будут всегда останавливаться. Их всего три операции. Константа(0), Функция Следования(инкремент +1) и собственно Функция Проекции (Рекурсия) которая все связывает. Три действия арифметики реализуются этими концептами. Их достаточно для реализации одного шага машины Тьюринга. Содержимое машины Тьюринга может быть представлено в виде очень большого числа и примитивные рекурсивные функции могут использоваться для чтения/записи или передвижения влево/вправо, но для полноценной работы машины Тьюринга необходимо больше. Поскольку они могут не останавливаться никогда. Также и с делением в арифметике. Когда появляется деление, то для этой операции необходима Функция Минимизации, которая уже не останавливается гарантировано. В случае же нуля, остановки не происходит, почему я и говорил, что деление на ноль и проблема остановки/тестирования это одна проблема по большому счету в Computer Science
Partial Recursive Functions
Отличная книга по этой теме.
Understanding Computation
Отрывок оттуда.
Сложение, умножение и вычитание можно получить в арифметике Пеано с помощью примитивных рекурсивных функций. И эти операции будут всегда останавливаться. Их всего три операции. Константа(0), Функция Следования(инкремент +1) и собственно Функция Проекции (Рекурсия) которая все связывает. Три действия арифметики реализуются этими концептами. Их достаточно для реализации одного шага машины Тьюринга. Содержимое машины Тьюринга может быть представлено в виде очень большого числа и примитивные рекурсивные функции могут использоваться для чтения/записи или передвижения влево/вправо, но для полноценной работы машины Тьюринга необходимо больше. Поскольку они могут не останавливаться никогда. Также и с делением в арифметике. Когда появляется деление, то для этой операции необходима Функция Минимизации, которая уже не останавливается гарантировано. В случае же нуля, остановки не происходит, почему я и говорил, что деление на ноль и проблема остановки/тестирования это одна проблема по большому счету в Computer Science
Partial Recursive Functions
Отличная книга по этой теме.
Understanding Computation
Отрывок оттуда.
Формальная верификация это и есть вычислительный аспект. Теорема Райса применима к ней.
На самом деле есть схемы, позволяющие примерно оценивать количество не найденных ошибок в программе. Они, естественно, не способны доказать отсутствие/наличие ошибок в программе, но позволяют оценить насколько якобы безбажный/малобажный продукт в реальности неидеален.
Да есть. Я сам когда то участвовал в разработке таких ассесмент систем для 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
Не помню деталей, но для проверки софта 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
Да, проблема нерешаема в общем виде. Но всегда ли нужен общий вид?
Дано: реализовать утилиту /bin/true.
Решение:
int main(void) { return 0; }
Найдите ошибку.
Дано: реализовать утилиту /bin/true.
Решение:
int main(void) { return 0; }
Найдите ошибку.
Не всегда нужен общий вид. Но даже в вашем выраженном примере в действительности выполняется не этот код. Он транслируется на все более низкие уровни абстракции, где последним уровнем являются по видимому электроны, которые подчиняются законам физики и выполняют computation. Но между вашим кодом и электронами множество слоев, в том числе и операционная система, и внутреннее устройство чипа и т.д. и т.п. Это все должно приниматься во внимание.
Бугаенко, не Бугаева)
Для понимания тестирования довольно-таки полезная статья. Автор молодец!
Sign up to leave a comment.
No Bugs, No Flaws или о надежности систем как таковых