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

Question

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

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

Например, классический вопрос FizzBuzz:

Напишите программу, которая печатает числа от 1 до 20. Но для кратных трех выведите «Fizz» вместо числа, а для кратных пяти выведите «Buzz». Для чисел, кратных трем и пяти, выведите «FizzBuzz».

и ниже это решение в Python:

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, и если это что-то, я могу использовать для решения этой проблемы.

Answer 1

Как упомянул Vilx, правильность программ (включая то, заканчиваются они или нет), как правило, неразрешима. Однако такие инструменты, как Z3, показывают, что соответствующие конкретные случаи все еще можно рассуждать, несмотря на общую неразрешимость проблемы.

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

Неисчерпывающий (и предвзятый) список ключевых слов для поиска: «статические анализаторы», «абстрактная интерпретация»; "facebook infer", "airbus absint", "juliasoft".

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

Неисчерпывающий (и предвзятый) список ключевых слов для поиска: «проверка», «логика хора», «логика разделения»; "eth viper", "microsoft dafny", "kuleuven validast", "microsoft f *".

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

Answer 2

Скажем так: математически доказано, что вы НЕ МОЖЕТЕ определить , если программа когда-либо прекратит работу.Поэтому, если вы хотите получить математически совершенный ответ, если целевая программа верна, вы обречены.

Тем не менее, вы все равно можете проводить модульные тесты и "линтинг", которые дадут вам множество интересных идей.

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