Разработка через тестирование и автоматическое доказательство теорем

Question

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

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

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

Answer 1

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

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

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

Answer 2

Звучит так, будто вы пытаетесь создать «математически проверенное программное обеспечение», чего очень трудно достичь.

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

Answer 3

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

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

Лично я бы просто использовал TDD - потому что его просто для меня и других прочитать кучу хорошо написанных тестов и выяснить, что делает код. Не говоря уже о быстрее тоже. Вам не нужно проверять все возможные выходные данные, а скорее определять репрезентативный набор входных данных. Каждый вход должен осуществлять различные результаты / путь через код.

Answer 4

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