Написать компьютерную программу, которая будет анализировать качество другой компьютерной программы?
Мне интересно узнать о возможностях этого. Я работаю над проектом, который проверяет навыки инженера-программиста, в настоящее время мы проверяем навыки на основе проверки кода сертифицированными разработчиками.
Я знаю ответ, если бы он был гораздо более полным, чем вопрос, я не мог представить, насколько сложной должна быть программа, чтобы анализировать сложный код, но я начинаю с основных вопросов интервью по программированию.
Например, классический вопрос FizzBuzz:
Напишите программу, которая печатает числа от 1 до 20. Но для числа, кратного трем, вместо числа печатайте «Шизз», а для числа, кратного пяти, печатайте «Жужжание». Для чисел, кратных как трем, так и пяти, выведите «FizzBuzz».
и ниже решение на питоне:
for num in range(1,21):
string = ""
if num % 3 == 0:
string = string + "Fizz"
if num % 5 == 0:
string = string + "Buzz"
if num % 5 != 0 and num % 3 != 0:
string = string + str(num)
print(string)Вопрос в том, можем ли мы программно проанализировать правильность этого решения?
Я хотел бы знать, пытался ли кто-нибудь это сделать, и есть ли текущие реализации, на которые я могу взглянуть. Также, если кто-то использовал z3, и если это то, что я могу использовать для решения этой проблемы.
Ответы 2
Скажем так: математически доказано, что вы НЕ МОЖЕМ определяете если программа, которая когда-либо завершится. Поэтому, если вам нужен математически совершенный ответ на вопрос, верна ли целевая программа, вы обречены.
Тем не менее, вы по-прежнему можете выполнять модульные тесты и «линтинг», которые дадут вам много интересной информации.
Но для простых фрагментов кода, таких как FizzBuzz, я думаю, что опытный разработчик, вероятно, даст наилучшие результаты.
Как упоминал Вилкс, правильность программ (включая то, завершаются они или нет) обычно неразрешима. Однако такие инструменты, как Z3, показывают, что о релевантных конкретных случаях все же можно рассуждать, несмотря на общую неразрешимость проблемы.
Статические анализаторы обычно ищет «простые» проблемы (например, нулевые разыменования, доступ за пределами границ, числовые переполнения), но они сравнительно быстры и требуют небольшого руководства пользователя (подумайте о руководстве в духе добавления аннотаций типов в ваш код).
Неполный (и необъективный) список ключевых слов для поиска: «статические анализаторы», «абстрактная интерпретация»; "выводы Facebook", "Airbus Absint", "juliasoft".
Верификаторы пытается доказать гораздо более богатые свойства, в частности функциональную правильность, например. «Действительно ли эта реализация сортировки сортирует мой массив (и не делает ничего другого, например, освобождает некоторую глобальную память или обновляет элемент, доступный из массива)?» или «действительно ли эта крипто-реализация реализует криптопротокол, который она обещает реализовать?». Это много более сложная задача, и инструменты из этого направления исследований, как правило, довольно медленные, требуют опытных пользователей с опытом формальной проверки и значительным руководством пользователя.
Неполный (и необъективный) список ключевых слов для поиска: «проверка», «логика хора», «логика разделения»; "eth viper", "microsoft dafny", "kuleuven verifast", "microsoft f*".
Существуют другие формальные методы, например. уточнение (или корректировка конструкции), но с еще меньшей инструментальной поддержкой и, насколько мне известно, признанием в отрасли.